English
The principal unit group of A is the subgroup of K× consisting of those x with valuation_A(x−1) < 1.
Русский
Главная единичная группа A — подгруппа K× из тех x, для которых v_A(x−1) < 1.
LaTeX
$$$A_{\mathrm{principalUnitGroup}} = \{x \in K^{\times} : v_A(x-1) < 1\}$$$
Lean4
/-- The principal unit group of a valuation subring, as a subgroup of `Kˣ`. -/
def principalUnitGroup : Subgroup Kˣ
where
carrier := {x | A.valuation (x - 1) < 1}
mul_mem' := by
intro a b ha hb
rw [Set.mem_setOf] at ha hb ⊢
refine lt_of_le_of_lt ?_ (max_lt hb ha)
rw [← one_mul (A.valuation (b - 1)), ← A.valuation.map_one_add_of_lt ha, add_sub_cancel, ← Valuation.map_mul,
mul_sub_one, ← sub_add_sub_cancel]
exact A.valuation.map_add _ _
one_mem' := by simp
inv_mem' := by
dsimp
intro a ha
conv =>
lhs
rw [← mul_one (A.valuation _), ← A.valuation.map_one_add_of_lt ha]
rwa [add_sub_cancel, ← Valuation.map_mul, sub_mul, Units.inv_mul, ← neg_sub, one_mul, Valuation.map_neg]
