Theorems · Theorem · commutative algebra

Subalgebra.rTensorBot_tmul

∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {A : Subalgebra R S} (x : R) (a : ↥A), A.rTensorBot (a ⊗ₜ[R] (algebraMap R ↥⊥) x) = x • a

Defined in

Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebra