one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val

English

For all e, (1 − X)^e · (invOneSubPow S (d + e)).val = (invOneSubPow S d).val.

Русский

Для любого e: (1 − X)^e · (invOneSubPow S (d + e)).val = (invOneSubPow S d).val.

LaTeX

$$$$ (1 - X)^e \cdot (invOneSubPow\, S\ (d+e)).\text{val} = (invOneSubPow\, S\ d).\text{val} $$$$

Lean4

theorem one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val (e : ℕ) :
    (1 - X) ^ e * (invOneSubPow S (d + e)).val = (invOneSubPow S d).val := by
  simp [invOneSubPow_add, Units.val_mul, mul_comm, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow]

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