lmul'' — Mathlib

English

The left and right tensor maps commute with scalar towers and preserve algebra structure.

Русский

Левые и правые тензорные отображения сохраняют структуру скаляров и алгебраическую структуру.

LaTeX

$$lmul''_toLinearEquiv := ...$$

Lean4

/-- `LinearMap.mul'` as an `AlgHom` over the algebra. -/
def lmul'' : S ⊗[R] S →ₐ[S] S :=
  algHomOfLinearMapTensorProduct
      { __ := LinearMap.mul' R S
        map_smul' := fun s x ↦
          x.induction_on (by simp) (fun _ _ ↦ by simp [TensorProduct.smul_tmul', mul_assoc]) fun x y hx hy ↦ by
            simp_all [mul_add] }
      (fun a₁ a₂ b₁ b₂ => by simp [mul_mul_mul_comm]) <|
    by simp

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