Mathlib Map

Theorems · Theorem · commutative algebra

expChar_ne_zero

∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [hR : ExpChar R p], p ≠ 0
Defined in
Mathlib.Algebra.CharP.Defs
Cited by
4 results in Mathlib
Foundations
Depth 23 from the axioms · uses propext
Assumes
AddMonoidWithOneExpChar
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

neg_one_pow_expChar_pow · cited by 2neg_one_pow_expChar_powAlgebra.trace_eq_zero_of_not_isSeparable · cited by 2Algebra.trace_eq_zero_of_…MvPowerSeries.map_frobenius_expand · cited by 1MvPowerSeries.map_frobeni…neg_one_pow_expChar · cited by 1neg_one_pow_expCharNat.Prime · cited by 2059Nat.PrimeCharZero · cited by 932CharZeroone_ne_zero · cited by 885one_ne_zeroCharP · cited by 478CharPAddMonoidWithOne · cited by 313AddMonoidWithOneExpChar · cited by 276ExpCharNat.Prime.ne_zero · cited by 109Prime.ne_zeroExpChar.casesOn · cited by 21ExpChar.casesOnexpChar_ne_zeroCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.