Theorems · Theorem · linear algebra

LinearMap.transvection.eq_id_of_finrank_le_one

∀ {R : Type u_3} {V : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  [Module.Free R V] [Module.Finite R V] [StrongRankCondition R] {f : Module.Dual R V} {v : V},
  f v = 0 → Module.finrank R V ≤ 1 → LinearMap.transvection f v = LinearMap.id

Defined in

Mathlib.LinearAlgebra.Transvection.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleModule.FreeModule.FiniteStrongRankCondition