English
Homogenizing a monomial of degree m inside two-variable polynomials yields a monomial with exponent m in the first variable and n−m in the second, times the same coefficient r.
Русский
Гомогенизация мономиала m в степени n даёт мономиал в двух переменных с степенью m в одной переменной и n−m в другой, с тем же коэффициентом r.
LaTeX
$$$\mathrm{homogenize}(\mathrm{monomial}(m,r))\, n = \mathrm{monomial}(m,\, n-m)\, r$$$
Lean4
/-- Given a polynomial `p` and a number `n ≥ natDegree p`,
returns a homogeneous bivariate polynomial `q` of degree `n` such that `q(x, 1) = p(x)`.
It is defined as `∑ k + l = n, a_k X_0^k X_1^l`, where `a_k` is the `k`th coefficient of `p`. -/
noncomputable def homogenize (p : R[X]) (n : ℕ) : MvPolynomial (Fin 2) R :=
∑ kl ∈ antidiagonal n, .monomial (fun₀ | 0 => kl.1 | 1 => kl.2) (p.coeff kl.1)
