quotEquivOfEqBot — Mathlib

English

If p = ⊥, then the quotient M/p is canonically isomorphic to M via the liftQ id construction.

Русский

Если p = ⊥, то фактор‑модуль M/p канонически изоморфен M через конструирование liftQ id.

LaTeX

$$$$ \\text{quotEquivOfEqBot} \\; (hp) : (M/ p) \\simeq M. $$$$

Lean4

/-- If `p = ⊥`, then `M / p ≃ₗ[R] M`. -/
def quotEquivOfEqBot (hp : p = ⊥) : (M ⧸ p) ≃ₗ[R] M :=
  LinearEquiv.ofLinear (p.liftQ id <| hp.symm ▸ bot_le) p.mkQ (liftQ_mkQ _ _ _) <|
    p.quot_hom_ext _ LinearMap.id fun _ => rfl

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