Theorems · Theorem · linear algebra

Matrix.ext_linearMap

∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_7} {β : Type u_8} [inst : DecidableEq m]
  [inst_1 : DecidableEq n] [Finite m] [Finite n] [inst_4 : Semiring R] [inst_5 : AddCommMonoid α]
  [inst_6 : AddCommMonoid β] [inst_7 : Module R α] [inst_8 : Module R β] ⦃f g : Matrix m n α →ₗ[R] β⦄,
  (∀ (i : m) (j : n), f ∘ₗ Matrix.singleLinearMap R i j = g ∘ₗ Matrix.singleLinearMap R i j) → f = g

Linear maps from finite matrices are equal if they agree on the standard basis. See note [partially-applied ext lemmas].

Defined in

Mathlib.Data.Matrix.Basis

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqFiniteFiniteSemiringAddCommMonoidAddCommMonoidModuleModule