mul_eq_closure_mul_set — Mathlib

English

For AddSubmonoids M,N of a nonunital nonassociative semiring R, the product M * N equals the closure of the set-theoretic product M * N viewed as a Set: M * N = closure(M * N : Set R).

Русский

Для аддитивных подподмножеств M и N кольца R удовлетворяется: M · N = closure(M · N : Set R).

LaTeX

$$$ M * N = \operatorname{closure}(M * N : Set R)$$$

Lean4

theorem mul_eq_closure_mul_set (M N : AddSubmonoid R) : M * N = closure (M * N : Set R) := by
  rw [← closure_mul_closure, closure_eq, closure_eq]

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