English
For valuation subrings A,B, B.principalUnitGroup ≤ A.principalUnitGroup iff A ≤ B.
Русский
Для подкольц A,B: B.principalUnitGroup ≤ A.principalUnitGroup тогда и только тогда, когда A ≤ B.
LaTeX
$${A B : ValuationSubring K} : B.principalUnitGroup ≤ A.principalUnitGroup ↔ A ≤ B$$
Lean4
theorem principalUnitGroup_le_principalUnitGroup {A B : ValuationSubring K} :
B.principalUnitGroup ≤ A.principalUnitGroup ↔ A ≤ B :=
by
constructor
· intro h x hx
by_cases h_1 : x = 0; · simp only [h_1, zero_mem]
by_cases h_2 : x⁻¹ + 1 = 0
· rw [add_eq_zero_iff_eq_neg, inv_eq_iff_eq_inv, inv_neg, inv_one] at h_2
simpa only [h_2] using B.neg_mem _ B.one_mem
· rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1, ← add_sub_cancel_right x⁻¹, ←
Units.val_mk0 h_2, ← mem_principalUnitGroup_iff] at hx ⊢
simpa only [hx] using @h (Units.mk0 (x⁻¹ + 1) h_2)
· intro h x hx
by_contra h_1; exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx
