mem_ofUnits_of_isUnit_of_unit_mem

English

Let S be a subgroup of the unit group Mˣ. If x ∈ M is a unit and its unit is contained in S, then x ∈ S.ofUnits.

Русский

Пусть S — подгруппа группы единиц Mˣ. Пусть x ∈ M является единицей и её соответствующая единица принадлежит S. Тогда x ∈ S.ofUnits.

LaTeX

$$$\\forall S \\ (S \\subseteq M^{\\times})\\ \\forall x\\in M:\\ IsUnit(x) \\land (x) \\in S \\Rightarrow x \\in S^{\\mathrm{ofUnits}}$$$

Lean4

@[to_additive]
theorem mem_ofUnits_of_isUnit_of_unit_mem (S : Subgroup Mˣ) {x : M} (h₁ : IsUnit x) (h₂ : h₁.unit ∈ S) :
    x ∈ S.ofUnits :=
  S.mem_ofUnits h₂ h₁.unit_spec

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