dual_comp — Mathlib

English

For linear maps f: A → B and g: B → C, the dual of the composite is the composition of the duals in reverse order: dual(g ∘ f) = (dual f) ∘ (dual g).

Русский

Для линейных отображений f: A → B и g: B → C выполняется dual(g ∘ f) = (dual f) ∘ (dual g).

LaTeX

$$$\mathrm{dual}(g \circ f) = (\mathrm{dual}(f)) \circ (\mathrm{dual}(g))$$$

Lean4

theorem dual_comp {C : Type*} [AddCommGroup C] [Module R C] (f : A →ₗ[R] B) (g : B →ₗ[R] C) :
    dual (g.comp f) = (dual f).comp (dual g) := by
  ext
  rfl

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