baseChange_lmul — Mathlib

English

Base change of the left multiplication map equals the left multiplication on the base-changed tensor product.

Русский

Замена основания левого умножения эквивалентна левой операции умножения на основание после базового изменения.

LaTeX

$$(Algebra.lmul R B f).baseChange A = Algebra.lmul A (A ⊗_R B) (1 ⊗ f)$$

Lean4

theorem baseChange_lmul {R B : Type*} [CommSemiring R] [Semiring B] [Algebra R B] {A : Type*} [CommSemiring A]
    [Algebra R A] (f : B) : (Algebra.lmul R B f).baseChange A = Algebra.lmul A (A ⊗[R] B) (1 ⊗ₜ f) :=
  by
  ext i
  simp

Похожие утверждения