smul'_mul — Mathlib

English

For x in T and p1,p2 in LocalizedModule S A, x • p1 * p2 = x • (p1 * p2); i.e., the scalar action distributes over multiplication.

Русский

Для x в T и p1,p2 в LocalizedModule S A, x • p1 * p2 = x • (p1 * p2); то есть скалярное действие распределяется по умножению.

LaTeX

$$$x \\cdot (p_1 p_2) = (x \\cdot p_1) p_2$$$

Lean4

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

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