Theorems · Theorem · linear algebra

TensorProduct.piScalarRight_apply

∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] (ι : Type u_4)
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] (x : TensorProduct R N (ι → R)),
  (TensorProduct.piScalarRight R S N ι) x = (TensorProduct.piScalarRightHom R S N ι) x

Defined in

Mathlib.LinearAlgebra.TensorProduct.Pi

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraAddCommMonoidModuleModuleIsScalarTowerFintypeDecidableEq