English
For a set S of places, the S-unit group in K× consists of those units that have valuation 1 at every place outside S; equivalently, it is the intersection of the unit groups coming from each valuation outside S.
Русский
Для множества S мест, группа S-единичных в K× состоит из тех единичных элементов, у которых при любой точке вне S показатель valuations равен 1; эквивалентно это пересечение групп единиц из каждой оценки за пределами S.
LaTeX
$$$S\text{.unit}(K)=\bigwedge_{v\notin S} (v.valuation(K).valuationSubring.\,unitGroup)$$$
Lean4
/-- The subgroup of `S`-units of `Kˣ`. -/
@[simps!]
def unit : Subgroup Kˣ :=
(⨅ (v) (_ : v ∉ S), (v.valuation K).valuationSubring.unitGroup).copy
{x : Kˣ | ∀ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuation K x = 1} <|
Set.ext fun _ => by simp only [mem_setOf, SetLike.mem_coe, Subgroup.mem_iInf, Valuation.mem_unitGroup_iff]
