toSubmodule_bot — Mathlib

English

The Submodule obtained from the bottom Subalgebra equals the whole module: Subalgebra.toSubmodule(⊥) = 1.

Русский

Подмодуль, полученный из нижней подпалгебры, равен всему модулю: Subalgebra.toSubmodule(⊥) = 1.

LaTeX

$$$\operatorname{toSubmodule}(\perp) = 1$$$

Lean4

/-- TODO: change proof to `rfl` when fixing https://github.com/leanprover-community/mathlib4/issues/18110. -/
theorem toSubmodule_bot : Subalgebra.toSubmodule (⊥ : Subalgebra R A) = 1 :=
  Submodule.one_eq_range.symm

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