Mathlib Map

Theorems · Theorem · number theory

MulChar.apply_mem_rootsOfUnity_orderOf

∀ {F : Type u_1} [inst : Field F] [Finite F] {R : Type u_2} [inst_2 : CommRing R] (χ : MulChar F R) {a : F},
  a ≠ 0 → ∃ ζ ∈ rootsOfUnity (orderOf χ) R, ↑ζ = χ a
Defined in
Mathlib.NumberTheory.MulChar.Lemmas
Cited by
1 results in Mathlib
Foundations
Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldFiniteCommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MulChar.apply_mem_rootsOfUnity_of_pow_eq_one · cited by 2MulChar.apply_mem_rootsOf…DFunLike.coe · cited by 62936DFunLike.coeCommRing · cited by 17173CommRingField · cited by 7404FieldSubgroup · cited by 3593SubgroupFinite · cited by 3029FiniteUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valIsUnit · cited by 1602IsUnitLT.lt.ne' · cited by 1417lt.ne'orderOf · cited by 324orderOfIsUnit.unit · cited by 252IsUnit.unitMulChar · cited by 186MulCharrootsOfUnity · cited by 118rootsOfUnityIsUnit.map · cited by 104IsUnit.mapNe.isUnit · cited by 99Ne.isUnitMulChar.apply_mem_rootsOfUnit…CITED BYCITES

Cites25

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

  • DFunLike.coestatement and proof · cited by 62,936
  • CommRingstatement and proof · cited by 17,173
  • Fieldstatement and proof · cited by 7,404
  • Subgroupstatement · cited by 3,593
  • Finitestatement and proof · cited by 3,029
  • Unitsstatement · cited by 2,804
  • Units.valstatement and proof · cited by 1,966
  • IsUnitproof · cited by 1,602
  • LT.lt.ne'proof · cited by 1,417
  • orderOfstatement and proof · cited by 324
  • IsUnit.unitproof · cited by 252
  • MulCharstatement and proof · cited by 186

Cited by1

Results whose statement or proof uses this declaration.