Theorems · Definition · algebraic geometry

Polynomial.homogenize

{R : Type u_1} → [inst : CommSemiring R] → Polynomial R → ℕ → MvPolynomial (Fin 2) R

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 kth coefficient of p.

Defined in

Mathlib.Algebra.Polynomial.Homogenize

Cited by

30 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring