Characteristic of semirings
- cast_eq_zero_iff : ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
The generator of the kernel of the unique homomorphism ℕ → α for a semiring α
Noncomputable function that outputs the unique characteristic of a semiring.
The frobenius map that sends x to x^p