English
Let E be a normed module and p a submodule with p = ⊤. Then the canonical linear isometry between p and E given by the inclusion is the identity map (under the natural identification of p with E).
Русский
Пусть E — нормированный модуль, p — подпространство such that p = ⊤. Тогда каноническая линейная изометрия между p и E, заданная включением, является тождественным отображением (после идентификации p с E).
LaTeX
$$$p = \\top \\Rightarrow \\text{ofTop}(p,hp) = \\mathrm{LinearIsometryEquiv.refl} R E$$$
Lean4
/-- If `p` is a submodule that is equal to `⊤`, then `LinearIsometryEquiv.ofTop p hp` is the
"identity" equivalence between `p` and `E`. -/
@[simps! toLinearEquiv apply symm_apply_coe]
def ofTop {R : Type*} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ⊤) : p ≃ₗᵢ[R] E :=
{ p.subtypeₗᵢ with toLinearEquiv := LinearEquiv.ofTop p hp }
