mul_smul' — Mathlib

English

For p1,p2 in LocalizedModule S A and x in T, p1 * x • p2 = x • (p1 * p2); a variant form of smul'_mul emphasizing left and right actions.

Русский

Для p1, p2 в LocalizedModule S A и x в T, p1 * x • p2 = x • (p1 * p2); вариация формы smul'_mul, подчёркивающая левое и правое действия.

LaTeX

$$$p_1 \\cdot x \\; \\mathrm{\\cdot} p_2 = x \\cdot (p_1 p_2)$$$

Lean4

theorem mul_smul' {A : Type*} [Semiring A] [Algebra R A] (x : T) (p₁ p₂ : LocalizedModule S A) :
    p₁ * x • p₂ = x • (p₁ * p₂) :=
  by
  induction p₁, p₂ using induction_on₂ with
  | _ a₁ s₁ a₂ s₂ => _
  rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]

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