English
There is a natural multiplicative equivalence between the S-unit group in K and the group of units of the ring of S-integers inside K.
Русский
Существует естественное умножительное эквивалентное отображение между S-единичными в K и группой единиц кольца S-интов в K.
LaTeX
$$$S.\text{unit}(K) \cong^* (S.\text{integer}(K))^{\times}$$$
Lean4
/-- The group of `S`-units is the group of units of the ring of `S`-integers. -/
@[simps apply_val_coe symm_apply_coe]
def unitEquivUnitsInteger : S.unit K ≃* (S.integer K)ˣ
where
toFun
x :=
⟨⟨((x : Kˣ) : K), fun v hv => (x.property v hv).le⟩, ⟨((x⁻¹ : Kˣ) : K), fun v hv => (x⁻¹.property v hv).le⟩,
Subtype.ext x.val.val_inv, Subtype.ext x.val.inv_val⟩
invFun
x :=
⟨Units.mk0 x fun hx => x.ne_zero (ZeroMemClass.coe_eq_zero.mp hx), fun v hv =>
eq_one_of_one_le_mul_left (x.val.property v hv) (x.inv.property v hv) <|
Eq.ge <| by rw [← map_mul, Units.val_mk0, Subtype.mk_eq_mk.mp x.val_inv, map_one]⟩
map_mul' _ _ := by ext; rfl
