sup_toAddSubgroup — Mathlib

English

The supremum of two submodules, when viewed as additive subgroups, equals the supremum in AddSubgroup structure.

Русский

Наибольший предел двух подмодулей, рассматриваемый как аддитивная подподгруппа, равен их пределу в структуре AddSubgroup.

LaTeX

$$ (p ⊔ p').toAddSubGroup = p.toAddSubGroup ⊔ p'.toAddSubGroup $$

Lean4

theorem sup_toAddSubgroup (p p' : Submodule R M) : (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup :=
  by
  ext x
  rw [mem_toAddSubgroup, mem_sup, AddSubgroup.mem_sup]
  rfl

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