Theorems · Theorem · linear algebra

Matrix.diagonal_map

∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : Zero β] {f : α → β},
  f 0 = 0 → ∀ {d : n → α}, (Matrix.diagonal d).map f = Matrix.diagonal fun m => f (d m)

Defined in

Mathlib.Data.Matrix.Diagonal

Cited by

15 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

DecidableEqZeroZero