compAlternatingMap — Mathlib

English

The sum of two alternating maps is alternating; the left-hand side equals the sum of the component maps.

Русский

Сумма двух чередующихся отображений снова чередующаяся; левая часть равна сумме компонентных отображений.

LaTeX

$$$ (f_1 + f_2) \circ_{\mathrm{Alt}} g = f_1 \circ_{\mathrm{Alt}} g + f_2 \circ_{\mathrm{Alt}} g $$$

Lean4

/-- Composing an alternating map with a linear map on the left gives again an alternating map. -/
def compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) : M [⋀^ι]→ₗ[R] N₂
    where
  __ := g.compMultilinearMap (f : MultilinearMap R (fun _ : ι => M) N)
  map_eq_zero_of_eq' v i j h hij := by simp [f.map_eq_zero_of_eq v h hij]

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