inf_toSubmodule — Mathlib

English

Let S and T be subalgebras of A. The underlying submodule of their meet equals the meet of their underlying submodules: toSubmodule(S ⊓ T) = toSubmodule(S) ⊓ toSubmodule(T).

Русский

Пусть S и T — подпалгебры A. Подмодульная часть их пересечения равна пересечению подмодулей: toSubmodule(S ⊓ T) = toSubmodule(S) ⊓ toSubmodule(T).

LaTeX

$$$\operatorname{toSubmodule}(S \cap T) = \operatorname{toSubmodule}(S) \cap \operatorname{toSubmodule}(T)$$$

Lean4

@[simp]
theorem inf_toSubmodule (S T : Subalgebra R A) : toSubmodule (S ⊓ T) = toSubmodule S ⊓ toSubmodule T :=
  rfl

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