comp_linearEquiv_eq_zero_iff — Mathlib

English

If we replace each argument by a linear equivalence, the zero-ness of the composed multilinear map is equivalent to the zero-ness of the original map.

Русский

Если заменить каждый аргумент линейным эквивалентом, нулевость композиции мультиленейной карты эквивалентна нулевости исходной карты.

LaTeX

$$$ (g.compLinearMap (\\λ i, (f i : M_i →ₗ[R] M_i'))) = 0 \\iff g = 0 $$$

Lean4

/-- Composing a multilinear map with a linear equiv on each argument gives the zero map
if and only if the multilinear map is the zero map. -/
@[simp]
theorem comp_linearEquiv_eq_zero_iff (g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i ≃ₗ[R] M₁' i) :
    (g.compLinearMap fun i => (f i : M₁ i →ₗ[R] M₁' i)) = 0 ↔ g = 0 :=
  by
  set f' := fun i => (f i : M₁ i →ₗ[R] M₁' i)
  rw [← zero_compLinearMap f', compLinearMap_inj f' fun i => (f i).surjective]

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