English
Describes how embDomain behaves under smul with powers: the embDomain of x multiplied by powers x matches a shifted subtraction by 1 in the domain, under a positivity assumption on x.
Русский
Определение поведения embDomain при умножении на мощности: embDomain при x со сдвигом соответствует вычитанию на 1 в домене, при условии положительности order.
LaTeX
$$$ (x \cdot powers x).embDomain \langle \mathrm{Nat}.succ, \mathrm{Nat}.succ_injective \rangle = powers x - ofFinsupp (Finsupp.single 0 1) $$$
Lean4
theorem embDomain_succ_smul_powers :
(x • powers x).embDomain ⟨Nat.succ, Nat.succ_injective⟩ = powers x - ofFinsupp (Finsupp.single 0 1) :=
by
apply SummableFamily.ext
rintro (_ | n)
· simp [hx]
· -- FIXME: smul_eq_mul introduces type confusion between HahnModule and HahnSeries.
simp [embDomain_apply, of_symm_smul_of_eq_mul, powers_of_orderTop_pos hx, pow_succ', -smul_eq_mul,
-Algebra.id.smul_eq_mul]
