Theorems · Theorem · linear algebra

Module.Basis.prod_apply

∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (i : ι ⊕ ι'),
  (b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i

Defined in

Mathlib.LinearAlgebra.Basis.Prod

Cited by

11 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule