eq_iff_principalUnitGroup — Mathlib

English

Two valuation subrings A and B of K are equal if and only if their principal unit groups are equal.

Русский

Два ценностных подкольца A и B поля K равны тогда и только тогда, когда их главные группы единиц совпадают.

LaTeX

$$$A = B \iff A.principalUnitGroup = B.principalUnitGroup$$$

Lean4

theorem eq_iff_principalUnitGroup {A B : ValuationSubring K} : A = B ↔ A.principalUnitGroup = B.principalUnitGroup :=
  principalUnitGroup_injective.eq_iff.symm

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