Mathlib Map

Theorems · Theorem · number theory

NumberField.IsCMField.unitsMulComplexConjInv_apply

∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K]
  (u : (NumberField.RingOfIntegers K)ˣ),
  ↑((NumberField.IsCMField.unitsMulComplexConjInv K) u) = u * ((NumberField.IsCMField.unitsComplexConj K) u)⁻¹
Defined in
Mathlib.NumberTheory.NumberField.CMField
Cited by
1 results in Mathlib
Foundations
Depth 309 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldCharZeroNumberField.IsCMFieldNumberField
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NumberField.IsCMField.unitsMulComplexConjInv_ker · cited by 1IsCMField.unitsMulComplex…DFunLike.coe · cited by 62936DFunLike.coeField · cited by 7404FieldMonoidHom · cited by 3629MonoidHomSubgroup · cited by 3593SubgroupUnits · cited by 2804UnitsMulEquiv · cited by 1142MulEquivCharZero · cited by 932CharZeroNumberField · cited by 653NumberFieldNumberField.RingOfIntegers · cited by 413NumberField.RingOfIntegersNumberField.Units.torsion · cited by 53Units.torsionNumberField.IsCMField · cited by 45NumberField.IsCMFieldNumberField.IsCMField.unitsMulComplexConjInv · cited by 9IsCMField.unitsMulComplex…NumberField.IsCMField.unitsComplexConj · cited by 5IsCMField.unitsComplexConjIsCMField.unitsMulComplexConj…CITED BYCITES

Cites13

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

Cited by1

Results whose statement or proof uses this declaration.