principal_units_le_units — Mathlib

English

For valuation subrings A,B, B.principalUnitGroup ≤ A.principalUnitGroup iff A ≤ B.

Русский

Для подкольц A,B: B.principalUnitGroup ≤ A.principalUnitGroup тогда и только тогда, когда A ≤ B.

LaTeX

$$$B_{\mathrm{principalUnitGroup}} \le A_{\mathrm{principalUnitGroup}} \iff A \le B$$$

Lean4

theorem principal_units_le_units : A.principalUnitGroup ≤ A.unitGroup := fun a h => by
  simpa only [add_sub_cancel] using A.valuation.map_one_add_of_lt h

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