Theorems · Theorem · linear algebra

AlternatingMap.compLinearEquiv_eq_zero_iff

∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (f : M [⋀^ι]→ₗ[R] N) (g : M₂ ≃ₗ[R] M), f.compLinearMap ↑g = 0 ↔ f = 0

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.

Defined in

Mathlib.LinearAlgebra.Alternating.Basic

Cited by

4 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModule