Theorems · Theorem · linear algebra

LinearMap.pi_ext

∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] [Finite ι] [inst_5 : AddCommMonoid M]
  [inst_6 : Module R M] {f g : ((i : ι) → φ i) →ₗ[R] M},
  (∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x)) → f = g

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

4 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEqFiniteAddCommMonoidModule