Theorems · Definition · commutative algebra
ringExpChar
(R : Type u_1) → [NonAssocSemiring R] → ℕ
Noncomputable function that outputs the unique exponential characteristic of a semiring.
- Defined in
- Mathlib.Algebra.CharP.Defs
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonAssocSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NonAssocSemiringstatement and proof · cited by 805
- ringCharproof · cited by 73
Cited by30
Results whose statement or proof uses this declaration.
- ringExpChar.eqstatement · cited by 15
- perfectClosureproof · cited by 14
- IsPurelyInseparable.minpoly_eqstatement and proof · cited by 3
- IsPurelyInseparable.elemExponent_le_of_pow_memstatement and proof · cited by 3
- IsPurelyInseparable.injective_comp_algebraMapproof · cited by 3
- IsPurelyInseparable.minpoly_natDegree_eqstatement and proof · cited by 2
- IsPurelyInseparable.HasExponent.has_exponentstatement · cited by 2
- IsPurelyInseparable.algebraMap_elemReduct_eqstatement and proof · cited by 2
- mem_perfectClosure_iffstatement · cited by 2
- map_mem_perfectClosure_iffproof · cited by 2
- le_perfectClosure_iffproof · cited by 2
- IsPurelyInseparable.exponent_defstatement · cited by 2