Theorems · Definition · linear algebra

Matrix.map

{m : Type u_2} → {n : Type u_3} → {α : Type v} → {β : Type w} → Matrix m n α → (α → β) → Matrix m n β

M.map f is the matrix obtained by applying f to each entry of the matrix M. This is available in bundled forms as: * AddMonoidHom.mapMatrix * LinearMap.mapMatrix * RingHom.mapMatrix * AlgHom.mapMatrix * Equiv.mapMatrix * AddEquiv.mapMatrix * LinearEquiv.mapMatrix * RingEquiv.mapMatrix * AlgEquiv.mapMatrix

Defined in

Mathlib.LinearAlgebra.Matrix.Defs

Cited by

247 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 61 definitions · uses Quot.sound