coe_quotEquivOfEqBot_symm — Mathlib

English

The inverse of the quotient isomorphism between M/p and M is the quotient projection; equivalently, the linear inverse map equals the projection M → M/p.

Русский

Обратное к изоморфизму фактор-модуля M/p и M есть проекция; эквивалентно, обратная линейная карта совпадает с отображением M → M/p.

LaTeX

$$$\bigl(\varphi_p: M/p \to M\bigr)^{-1} = p.mkQ : M \to M/p,$$$

Lean4

@[simp]
theorem coe_quotEquivOfEqBot_symm (hp : p = ⊥) : ((p.quotEquivOfEqBot hp).symm : M →ₗ[R] M ⧸ p) = p.mkQ :=
  rfl

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