Theorems · Theorem · linear algebra

Module.Basis.repr_apply_eq

∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (f : M → ι → R),
  (∀ (x y : M), f (x + y) = f x + f y) →
    (∀ (c : R) (x : M), f (c • x) = c • f x) →
      (∀ (i : ι), f (b i) = ⇑fun₀ | i => 1) → ∀ (x : M) (i : ι), (b.repr x) i = f x i

An unbundled version of repr_eq_iff

Defined in

Mathlib.LinearAlgebra.Basis.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule