unit_eq — Mathlib

English

The S-unit group equals the infimum of the unit groups corresponding to each valuation v outside S.

Русский

Группа S-единичных равна точному наименьшему общему делителю (наибольшему подпрегоне) групп единиц, соответствующих каждой оценке v вне S.

LaTeX

$$$S.\text{unit}(K)=\bigwedge_{v\notin S} (v.valuation(K).valuationSubring.\,unitGroup)$$$

Lean4

theorem unit_eq : S.unit K = ⨅ (v) (_ : v ∉ S), (v.valuation K).valuationSubring.unitGroup :=
  Subgroup.copy_eq _ _ _

Похожие утверждения