Theorems · Definition · linear algebra

Matrix.of

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

Cast a function into a matrix. The two sides of the equivalence are definitionally equal types. We want to use an explicit cast to distinguish the types because Matrix has different instances to pi types (such as Pi.mul, which performs elementwise multiplication, vs Matrix.mul). If you are defining a matrix, in terms of its entries, use of (fun i j ↦ _). The purpose of this approach is to ensure that terms of the form (fun i j ↦ _) * (fun i j ↦ _) do not appear, as the type of * can be misleading.

Defined in

Mathlib.LinearAlgebra.Matrix.Defs

Cited by

336 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 40 definitions · uses no axioms