Mathlib Map

Theorems · Theorem · commutative algebra

ringExpChar.of_eq

∀ {R : Type u_1} [inst : Ring R] [IsDomain R] {q : ℕ}, ringExpChar R = q → ExpChar R q
Defined in
Mathlib.Algebra.CharP.Defs
Cited by
1 results in Mathlib
Foundations
Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
RingIsDomain
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ringExpChar.eq_iff · cited by 0ringExpChar.eq_iffRing · cited by 7463RingIsDomain · cited by 2196IsDomainExpChar · cited by 276ExpCharringExpChar · cited by 27ringExpCharringExpChar.of_eqCITED BYCITES

Cites4

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

  • Ringstatement and proof · cited by 7,463
  • IsDomainstatement and proof · cited by 2,196
  • ExpCharstatement · cited by 276
  • ringExpCharstatement and proof · cited by 27

Cited by1

Results whose statement or proof uses this declaration.