Theorems · Theorem · number theory

NumberField.IsCMField.closure_realFundSystem_sup_torsion

∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  Subgroup.closure (Set.range (NumberField.IsCMField.realFundSystem K)) ⊔ NumberField.Units.torsion K =
    NumberField.IsCMField.realUnits K ⊔ NumberField.Units.torsion K

Defined in: Mathlib.NumberTheory.NumberField.CMField
Cited by: 1 results in Mathlib
Foundations: Depth 328 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field CharZero NumberField.IsCMField NumberField

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites40

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

DFunLike.coeproof · cited by 62,936
Setproof · cited by 53,352
SetLike.coeproof · cited by 8,199
Fieldstatement and proof · cited by 7,404
Groupproof · cited by 6,238
Set.imageproof · cited by 5,609
Algebra.algebraMapproof · cited by 4,706
Set.rangestatement and proof · cited by 4,705
Equiv.symmproof · cited by 3,681
MonoidHomproof · cited by 3,629
Subgroupstatement and proof · cited by 3,593
Unitsstatement and proof · cited by 2,804

Cited by1

Results whose statement or proof uses this declaration.

NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_invproof · cited by 0