mul_dpow — Mathlib

English

For m, a, x with x ∈ I, dpow I m (a × x) equals a^m times dpow I m x.

Русский

Для m, a и x с x ∈ I, dpow I m (a × x) = a^m · dpow I m x.

LaTeX

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

Lean4

theorem mul_dpow {n : ℕ} (hn_fac : IsUnit ((n - 1).factorial : A)) (hnI : I ^ n = 0) {m k : ℕ} {x : A} (hx : x ∈ I) :
    dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x :=
  by
  by_cases hkm : m + k < n
  · exact dpow_mul_of_add_lt hn_fac hkm hx
  · have hxmk : x ^ (m + k) = 0 := Ideal.pow_eq_zero_of_mem hnI (not_lt.mp hkm) hx
    rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx, mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m),
      mul_assoc _ (x ^ m), ← pow_add, hxmk, mul_zero, mul_zero, mul_zero, mul_zero]

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