subsingleton_normalizedGCDMonoid_of_unique_units

English

If α has a subsingleton of units, then the gcd-monoid structure on α is unique.

Русский

Если у α единицы образуют подсинглтоны, то структура gcd-моноида на α уникальна.

LaTeX

$$$$ \\text{If } \\lvert Units(\\alpha) \\rvert = 1, \\text{ then } \\text{GCDMonoid}(\\alpha) \\text{ is unique}. $$$$

Lean4

instance subsingleton_normalizedGCDMonoid_of_unique_units : Subsingleton (NormalizedGCDMonoid α) :=
  ⟨by
    intro a b
    cases a; rename_i a_norm a_gcd _ _
    cases b; rename_i b_norm b_gcd _ _
    have := Subsingleton.elim a_gcd b_gcd
    subst this
    have := Subsingleton.elim a_norm b_norm
    subst this
    rfl⟩

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