postcomp_apply — Mathlib

English

Postcomposition of an alternating map by a linear map is given by composing with the linear map on the output.

Русский

Постпокомпозиция чередующегося отображения линейным отображением получается как композиция с этим отображением на выходе.

LaTeX

$$φ.postcomp g = g.hom ∘ φ$$

Lean4

@[simp]
theorem postcomp_apply (x : Fin n → M) : φ.postcomp g x = g (φ x) :=
  rfl

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