coe_closure_eq — Mathlib

English

The elements of the subsemiring closure of s are exactly the elements of the additive closure of the multiplicative closure of s.

Русский

Элементы замыкания подsemiring множества s совпадают с элементами аддитивного замыкания мультипликативного замыкания s.

LaTeX

$$$\\operatorname{closure}(s) = AddSubmonoid.closure (Submonoid.closure s : Set R)$$$

Lean4

/-- The elements of the subsemiring closure of `M` are exactly the elements of the additive closure
of a multiplicative submonoid `M`. -/
theorem coe_closure_eq (s : Set R) : (closure s : Set R) = AddSubmonoid.closure (Submonoid.closure s : Set R) := by
  simp [← Submonoid.subsemiringClosure_toAddSubmonoid, Submonoid.subsemiringClosure_eq_closure]

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