quotientInfEquivSupQuotient_symm_apply_eq_zero_iff

Mathlib.LinearAlgebra.Isomorphisms

URI: https://scilib.ai/kg/mathlib#LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff

← MathLib Explorer

English

The map quotientInfToSupQuotient is injective.

Русский

Отображение quotientInfToSupQuotient инъективно.

LaTeX

$$Theorem: Function.Injective (quotientInfToSupQuotient p p')$$

Lean4

theorem quotientInfEquivSupQuotient_symm_apply_eq_zero_iff {p p' : Submodule R M} {x : ↥(p ⊔ p')} :
    (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ (x : M) ∈ p' :=
  (LinearEquiv.symm_apply_eq _).trans <| by simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru