Mathlib Map

Theorems · Theorem · commutative algebra

CharP.cast_eq_zero

∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p], ↑p = 0
Defined in
Mathlib.Algebra.CharP.Defs
Cited by
357 results in Mathlib
Foundations
Depth 19 from the axioms, rests on 136 definitions · uses propext
Assumes
AddMonoidWithOneCharP
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Real.log_pow · cited by 29Real.log_powENNReal.rpow_natCast · cited by 18ENNReal.rpow_natCastZMod.natCast_self · cited by 15ZMod.natCast_selfdescPochhammer_succ_right · cited by 14descPochhammer_succ_rightascPochhammer_succ_right · cited by 11ascPochhammer_succ_rightContDiffWithinAt.continuousWithinAt · cited by 11ContDiffWithinAt.continuo…CharP.eq · cited by 9CharP.eqbernoulli'_zero · cited by 9bernoulli'_zeroComplex.differentiableAt_Gamma · cited by 8Complex.differentiableAt_…ZMod.unitsMap_surjective · cited by 7ZMod.unitsMap_surjectivePolynomial.Chebyshev.degree_T · cited by 7Chebyshev.degree_TMatrix.zpow_neg_natCast · cited by 6Matrix.zpow_neg_natCastPolynomial.isEquivalent_atTop_div · cited by 5Polynomial.isEquivalent_a…add_pow_expChar_of_commute · cited by 5add_pow_expChar_of_commuteadd_pow_expChar_pow_of_commute · cited by 5add_pow_expChar_pow_of_co…CharP · cited by 478CharPAddMonoidWithOne · cited by 313AddMonoidWithOnedvd_rfl · cited by 80dvd_rflCharP.cast_eq_zero_iff · cited by 42CharP.cast_eq_zero_iffCharP.cast_eq_zeroCITED BYCITES

Cites4

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

Cited by357

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 357.