baseChange_bot — Mathlib

English

The base change of the zero submodule is again the zero submodule.

Русский

Базовое изменение нулевого подмодуля снова является нулевым подмодулем.

LaTeX

$$$ (\\bot : \\mathrm{LieSubmodule\\} R L M)^{\\mathrm{baseChange}_A} = \\bot $$$

Lean4

@[simp]
theorem baseChange_bot : (⊥ : LieSubmodule R L M).baseChange A = ⊥ :=
  by
  simp only [baseChange, bot_toSubmodule, Submodule.baseChange_bot]
  rfl

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