dpow_mul — Mathlib

English

In a divided powers context, multiplying x by an element in the ideal scales the m-th divided power by a^m.

Русский

В контексте разделённых степеней умножение x на элемент I масштабирует m-ю делённую степень на a^m.

LaTeX

$$$dpow I m (a \cdot x) = a^m \cdot dpow I m x$$$

Lean4

theorem dpow_mul {m : ℕ} {a x : A} (hx : x ∈ I) : dpow I m (a * x) = a ^ m * dpow I m x := by
  rw [dpow_eq_of_mem (Ideal.mul_mem_left I _ hx), dpow_eq_of_mem hx, mul_pow, ← mul_assoc, mul_comm _ (a ^ m),
    mul_assoc]

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