sumSq_toAddSubmonoid — Mathlib

English

The submonoid generated by sums of squares is the same as the sumSq submonoid; i.e., (sumSq T).toAddSubmonoid = .sumSq T.

Русский

Подмножество, порождаемое суммами квадратов, совпадает с подмодуляцией сумм квадратов; то есть (sumSq T).toAddSubmonoid = .sumSq T.

LaTeX

$$$ (\operatorname{sumSq} T).\mathrm{toAddSubmonoid} = \mathrm{AddSubmonoid}.sumSq\ T $$$

Lean4

@[simp]
theorem sumSq_toAddSubmonoid : (sumSq T).toAddSubmonoid = .sumSq T := by
  simp [sumSq, ← AddSubmonoid.closure_isSquare, Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid]

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