LocalRing

Statistics

Metric	Count
Definitions	0
Theorems `charP_zero_or_prime_power`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`charP_zero_or_prime_power` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero`	—	`CharP.char_is_prime_or_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ringChar.charP` `Nat.ordProj_dvd` `Nat.not_dvd_ordCompl` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq_zero_iff_mem` `IsLocalRing.mem_maximalIdeal` `mem_nonunits_iff` `ringChar.spec` `map_natCast` `RingHom.instRingHomClass` `one_mul` `IsUnit.val_inv_mul` `mul_assoc` `Nat.cast_mul` `mul_comm` `CharP.cast_eq_zero` `MulZeroClass.mul_zero` `CharP.cast_eq_zero_iff` `pow_zero` `CharP.char_ne_one` `Nat.Prime.prime` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `CharP.eq` `CharP.ofCharZero` `RingHom.charZero` `CharP.charP_to_charZero` `ringChar.of_eq`

---