comap_dualAnnihilator — Mathlib

English

The comap along Dual.eval of the dual annihilator equals the dual coannihilator.

Русский

Comap вдоль Dual.eval от дуального аннигилятора равен дуальному коаннигилятору.

LaTeX

$$Submodule.comap_dualAnnihilator (Φ : Submodule R (Module.Dual R M)) : Φ.dualAnnihilator.comap (Module.Dual.eval R M) = Φ.dualCoannihilator$$

Lean4

theorem comap_dualAnnihilator (Φ : Submodule R (Module.Dual R M)) :
    Φ.dualAnnihilator.comap (Module.Dual.eval R M) = Φ.dualCoannihilator :=
  rfl

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