Theorems · Theorem · linear algebra

Matrix.range_diagonal

∀ {m : Type u_1} [inst : Fintype m] {K : Type u} [inst_1 : Semifield K] [inst_2 : DecidableEq m] (w : m → K),
  (Matrix.toLin' (Matrix.diagonal w)).range = ⨆ i ∈ {i | w i ≠ 0}, (LinearMap.single K (fun x => K) i).range

Defined in

Mathlib.LinearAlgebra.Matrix.Diagonal

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeSemifieldDecidableEq