English
Let D: A → B be an injective map preserving addition (i.e., D(a1 + a2) = D(a1) + D(a2)). For p, q in the monoid algebra R[A], the value of p*q at the degree D^{-1}(supDegree_D(p) + supDegree_D(q)) equals the product of the leading coefficients of p and q with respect to D.
Русский
Пусть D: A → B инъективна и сохраняет сложение (D(a1 + a2) = D(a1) + D(a2)). Для p, q из алгебры Моноида над A над R верно, что значение p·q в элементе D^{-1}(supDegree_D(p) + supDegree_D(q)) равно произведению ведущих коэффициентов p и q относительно D.
LaTeX
$$$$(p * q)\bigl(D^{-1}(\operatorname{supDegree}_D(p) + \operatorname{supDegree}_D(q))\bigr) = \operatorname{leadingCoeff}_D(p) \cdot \operatorname{leadingCoeff}_D(q)$$$$
Lean4
theorem apply_supDegree_add_supDegree (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) :
(p * q) (D.invFun (p.supDegree D + q.supDegree D)) = p.leadingCoeff D * q.leadingCoeff D :=
by
obtain rfl | hp := eq_or_ne p 0
· simp_rw [leadingCoeff_zero, zero_mul, Finsupp.coe_zero, Pi.zero_apply]
obtain rfl | hq := eq_or_ne q 0
· simp_rw [leadingCoeff_zero, mul_zero, Finsupp.coe_zero, Pi.zero_apply]
obtain ⟨ap, -, hp⟩ := exists_supDegree_mem_support D hp
obtain ⟨aq, -, hq⟩ := exists_supDegree_mem_support D hq
simp_rw [leadingCoeff, hp, hq, ← hadd, Function.leftInverse_invFun hD _]
exact apply_add_of_supDegree_le hadd hD hp.le hq.le
