quotDualCoannihilatorToDual_injective

English

The flipped map is injective, meaning viewing the dual map in the opposite order preserves distinctness.

Русский

Перевёрнутое отображение инъективно, то есть сохранение различности при смене порядка отображения.

LaTeX

$$Function.Injective(W.quotDualCoannihilatorToDual.flip)$$

Lean4

theorem quotDualCoannihilatorToDual_injective (W : Submodule R (Dual R M)) :
    Function.Injective W.quotDualCoannihilatorToDual :=
  LinearMap.ker_eq_bot.mp (ker_liftQ_eq_bot _ _ _ le_rfl)

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