span_int_eq — Mathlib

English

Similarly, span Int for AddSubgroup equals the AddSubgroup closure.

Русский

Аналогично, span Int для AddSubgroup совпадает с замыканием AddSubgroup.

LaTeX

$$$$ (\operatorname{span} \mathbb{Z} (s : Set M)).toAddSubgroup = \operatorname{AddSubgroup}.closure s $$$$

Lean4

@[simp]
theorem span_int_eq {M : Type*} [AddCommGroup M] (s : AddSubgroup M) : (span ℤ (s : Set M)).toAddSubgroup = s := by
  rw [span_int_eq_addSubgroupClosure, s.closure_eq]

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