Theorems · Theorem · linear algebra

Matrix.map_one

∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] [inst_3 : Zero β]
  [inst_4 : One β] (f : α → β), f 0 = 0 → f 1 = 1 → Matrix.map 1 f = 1

Defined in

Mathlib.Data.Matrix.Diagonal

Cited by

15 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroOneZeroOne