mem_toAddSubgroup — Mathlib

English

Membership in the additive subgroup corresponding to a subring matches membership in the subring itself.

Русский

Членство в аддитивной подпогруппе, соответствующей подкольцу, совпадает с членством в самом подкольце.

LaTeX

$$$x\in s^{\mathrm{toAddSubgroup}} \iff x\in s$$$

Lean4

theorem mem_toAddSubgroup {s : Subring R} {x : R} : x ∈ s.toAddSubgroup ↔ x ∈ s :=
  Iff.rfl

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