curryLeft_compLinearMap — Mathlib

English

Let g be a linear map from M₂ to M and f an alternating map from M to N. Then curryLeft distributes over precomposition by g: (f∘g).curryLeft m equals (f.curryLeft (g m))∘g.

Русский

Пусть g: M₂ → M, f: M →⋄ N является чередующейся. Тогда curryLeft распределяется по предварительной композиции: (f∘g).curryLeft m = (f.curryLeft (g m))∘g.

LaTeX

$$$$\forall (g: M_2 \toₗ[R] M) (f: M [⋀^Fin n.succ]→ₗ[R] N) (m: M_2),\\ (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g.$$$$

Lean4

@[simp]
theorem curryLeft_compLinearMap (g : M₂ →ₗ[R] M) (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M₂) :
    (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g :=
  ext fun v ↦ congr_arg f <| funext fun i ↦ by cases i using Fin.cases <;> simp

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