Theorems · Theorem · linear algebra

LinearMap.rank_zero

∀ {K : Type u} {V : Type v} {V' : Type v'} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V'] [inst_4 : Module K V'] [Nontrivial K], LinearMap.rank 0 = 0

Defined in

Mathlib.LinearAlgebra.Dimension.LinearMap

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModuleNontrivial