square_toSubmonoid — Mathlib

English

In a commutative group G, the submonoid generated by the squares coincides with the set of all squares; i.e., the underlying monoid of the square subgroup equals the square-submonoid.

Русский

В коммутативной группе G подмножество, порождённое квадратами, совпадает с множеством всех квадратов; то есть подмножество, лежащее в квадратной подсистеме, совпадает с множеством квадратов.

LaTeX

$$$ (\\mathrm{square}\\, G).\\text{toSubmonoid} = \\text{.square } G $$$

Lean4

@[to_additive (attr := simp)]
theorem square_toSubmonoid : (square G).toSubmonoid = .square G :=
  rfl

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