Theorems · Theorem · commutative algebra

Algebra.baseChange_lmul

∀ {R : Type u_1} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Algebra R B] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (f : B),
  LinearMap.baseChange A ((Algebra.lmul R B) f) = (Algebra.lmul A (TensorProduct R A B)) (1 ⊗ₜ[R] f)

Defined in

Mathlib.RingTheory.TensorProduct.Basic

Cited by

1 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebraCommSemiringAlgebra