coe_bot — Mathlib

English

The underlying submodule of the bottom element equals the zero subspace, i.e., the bottom is realized by {0}.

Русский

Основанное подпространство нижнего элемента равно нулевому подпространству: нижняя граница — {0}.

LaTeX

$$$(\\uparrow(\\bottom : \\rho.invtSubmodule) : Submodule k V) = \\bot$$$

Lean4

@[simp]
protected theorem coe_bot : (↑(⊥ : ρ.invtSubmodule) : Submodule k V) = ⊥ :=
  rfl

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