Theorems · Theorem · linear algebra

mulLeftLinearMap_eq_zero_iff

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_5} {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : Semiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A] [Nonempty n] (a : Matrix l m A),
  mulLeftLinearMap n R a = 0 ↔ a = 0

A version of LinearMap.mulLeft_eq_zero_iff for matrix multiplication.

Defined in

Mathlib.LinearAlgebra.Matrix.Bilinear

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeSemiringSemiringModuleSMulCommClassNonempty