closure_isSquare — Mathlib

English

In a commutative semiring, the closure of the set of squares equals sumSq; i.e., closure { x | IsSquare x } = sumSq T.

Русский

В коммутативном полускольном кольце замыкание множества квадратов равно sumSq.

LaTeX

$$$\operatorname{closure}\{ x : T \mid \operatorname{IsSquare}(x) \} = \operatorname{sumSq} T$$$

Lean4

@[simp]
theorem closure_isSquare : closure {x : T | IsSquare x} = sumSq T := by
  simp [sumSq, Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]

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