compLinearEquiv_eq_zero_iff — Mathlib

English

Composing with a linear equivalence on the domain yields zero iff the original alternating map is zero.

Русский

Композиция с линейной эквивалентностью домена даёт ноль тогда и только тогда, когда исходная чередующаяся карта нулевая.

LaTeX

$$f.compLinearMap g = 0 \\iff f = 0$$

Lean4

/-- Composing an alternating map with the same linear equiv on each argument gives the zero map
if and only if the alternating map is the zero map. -/
@[simp]
theorem compLinearEquiv_eq_zero_iff (f : M [⋀^ι]→ₗ[R] N) (g : M₂ ≃ₗ[R] M) :
    f.compLinearMap (g : M₂ →ₗ[R] M) = 0 ↔ f = 0 :=
  (domLCongr R N ι ℕ g.symm).map_eq_zero_iff

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