one_sub_self_mul_hsum_powers — Mathlib

English

If 0 < x.orderTop, then (1 - x) * (powers x).hsum = 1, i.e., the inverse relation holds via the hsum of powers.

Русский

Если 0 < x.orderTop, то (1 - x) * (powers x).hsum = 1.

LaTeX

$$$0 < x.orderTop \Rightarrow (1 - x) \cdot (powers x).hsum = 1$$$

Lean4

theorem one_sub_self_mul_hsum_powers : (1 - x) * (powers x).hsum = 1 :=
  by
  rw [← hsum_smul, sub_smul 1 x (powers x), one_smul, hsum_sub, ←
    hsum_embDomain (x • powers x) ⟨Nat.succ, Nat.succ_injective⟩, embDomain_succ_smul_powers hx]
  simp

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