mul_toSubmodule_le — Mathlib

English

The product of the submodules underlying two subalgebras is contained in the submodule underlying their join.

Русский

Произведение подмодулей двух подалгебр содержится в подмодуле их объединения.

LaTeX

$$(toSubmodule S) * (toSubmodule T) \le toSubmodule(S ⊔ T)$$

Lean4

theorem mul_toSubmodule_le (S T : Subalgebra R A) :
    (Subalgebra.toSubmodule S) * (Subalgebra.toSubmodule T) ≤ Subalgebra.toSubmodule (S ⊔ T) :=
  by
  rw [Submodule.mul_le]
  intro y hy z hz
  change y * z ∈ S ⊔ T
  exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)

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