inf_toSubmodule — Mathlib

English

The underlying Submodule of the infimum equals the intersection of the underlying Submodules; i.e., N ∩ N' corresponds accordingly.

Русский

Основанный подмодуль нижнего предела равен пересечению подмодулей.

LaTeX

$$$ (N \sqcap N')^{toSubmodule} = N^{toSubmodule} \cap N'^{toSubmodule} $$$

Lean4

@[norm_cast, simp]
theorem inf_toSubmodule : (↑(N ⊓ N') : Submodule R M) = (N : Submodule R M) ⊓ (N' : Submodule R M) :=
  rfl

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