mem_ofUnits_iff_exists_isUnit — Mathlib

English

For a subgroup S of Mˣ and an element x ∈ M, x is in S.ofUnits if and only if there exists a unit h with h.unit ∈ S and h corresponds to x as a unit.

Русский

Для подгруппы S подпмножества единиц Mˣ и элемента x ∈ M справедливо: x ∈ S.ofUnits тогда и только тогда, когда существует единица h, такая что h.unit ∈ S и h соответствует x как единица.

LaTeX

$$$x \\in S^{\\mathrm{ofUnits}} \\iff \\exists h : IsUnit(x), h.unit \\in S$$$

Lean4

@[to_additive]
theorem mem_ofUnits_iff_exists_isUnit (S : Subgroup Mˣ) (x : M) : x ∈ S.ofUnits ↔ ∃ h : IsUnit x, h.unit ∈ S :=
  ⟨fun h => ⟨S.isUnit_of_mem_ofUnits h, S.unit_mem_of_mem_ofUnits h⟩, fun ⟨hm, he⟩ =>
    S.mem_ofUnits_of_isUnit_of_unit_mem hm he⟩

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