subsemiringClosure_eq_closure — Mathlib

English

The nonunital version of the subsemiring closure of M coincides with the nonunital closure of M.

Русский

Ненулевое замыкание подsemiring M совпадает с ненулевым замыканием M.

LaTeX

$$M.subsemiringClosure.toNonUnitalSubsemiring = NonUnitalSubsemiring.closure (Submonoid.instSetLike.coe M)$$

Lean4

/-- The `Subsemiring` generated by a multiplicative submonoid coincides with the
`Subsemiring.closure` of the submonoid itself . -/
theorem subsemiringClosure_eq_closure : M.subsemiringClosure = Subsemiring.closure (M : Set R) :=
  by
  ext
  refine ⟨fun hx => ?_, fun hx => (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => ?_⟩ <;>
      rintro - ⟨H1, rfl⟩ <;>
    rintro - ⟨H2, rfl⟩
  · exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2
  · exact H2 sM

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