inf_toSubmodule — Mathlib

English

The infimum of subalgebras, taken as submodules, coincides with the infimum of the corresponding submodules.

Русский

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

LaTeX

$$$ (S, T)\\; (S \\inf T).toSubmodule = S.toSubmodule \\inf T.toSubmodule $$$

Lean4

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

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