Characteristic of semirings #
theorem
CharP.char_ne_zero_of_finite
(R : Type u_1)
[NonAssocRing R]
(p : ℕ)
[CharP R p]
[Finite R]
:
The characteristic of a finite ring cannot be zero.
theorem
CharP.char_is_prime
(R : Type u_1)
[Ring R]
[NoZeroDivisors R]
[Nontrivial R]
[Finite R]
(p : ℕ)
[CharP R p]
:
The Frobenius map x ↦ x ^ p
.
Equations
- frobenius R p = { toMonoidHom := powMonoidHom p, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The iterated Frobenius map x ↦ x ^ p ^ n
.
Equations
- iterateFrobenius R p n = { toMonoidHom := powMonoidHom (p ^ n), map_zero' := ⋯, map_add' := ⋯ }
Instances For
theorem
multiset_sum_pow_char
{R : Type u_3}
[CommSemiring R]
(p : ℕ)
[ExpChar R p]
(s : Multiset R)
:
theorem
multiset_sum_pow_char_pow
{R : Type u_3}
[CommSemiring R]
(p n : ℕ)
[ExpChar R p]
(s : Multiset R)
: