quotDualCoannihilatorToDual_apply

English

The map from M to its dual via the quotient by the dual coannihilator is injective.

Русский

Отображение через фактор-модуль по двойственному коаннигилятору инъективно.

LaTeX

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

Lean4

@[simp]
theorem quotDualCoannihilatorToDual_apply (W : Submodule R (Dual R M)) (m : M) (w : W) :
    W.quotDualCoannihilatorToDual (Quotient.mk m) w = w.1 m :=
  rfl

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