dualMap_trans — Mathlib

English

For linear equivalences f: M1 ≃ M2 and g: M2 ≃ M3, the dual maps satisfy g.dualMap.trans f.dualMap = (f.trans g).dualMap.

Русский

Для линейных эквивалентов f: M1 ≃ M2, g: M2 ≃ M3 выполняется g.dualMap.trans f.dualMap = (f.trans g).dualMap.

LaTeX

$$$$ g.dualMap.trans f.dualMap = (f.trans g).dualMap. $$$$

Lean4

theorem dualMap_trans {M₃ : Type*} [AddCommMonoid M₃] [Module R M₃] (f : M₁ ≃ₗ[R] M₂) (g : M₂ ≃ₗ[R] M₃) :
    g.dualMap.trans f.dualMap = (f.trans g).dualMap :=
  rfl

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