Commit 2025-10-30 10:43 68abb997

View on Github →

feat: SkewPolynomial (#29300)

Univariate skew polynomials

Skew polynomials are represented as SkewMonoidAlgebra R (Multiplicative ℕ), where R is usually at least a Semiring. In this file, we define SkewPolynomial and provide basic instances. The point if this PR is to introduce the very most basic definitions and API. From #23949.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

modified def SkewMonoidAlgebra.support

added theorem SkewMonoidAlgebra.support_add

Created Mathlib/Algebra/SkewPolynomial/Basic.lean

added theorem SkewPolynomial.card_support_eq_zero

added def SkewPolynomial.monomial

added theorem SkewPolynomial.monomial_add

added theorem SkewPolynomial.monomial_def

added theorem SkewPolynomial.monomial_mul_monomial

added theorem SkewPolynomial.monomial_zero_one

added theorem SkewPolynomial.monomial_zero_right

added theorem SkewPolynomial.smul_monomial

added def SkewPolynomial.support

added theorem SkewPolynomial.support_add

added theorem SkewPolynomial.support_eq_empty

added theorem SkewPolynomial.support_zero

added theorem SkewPolynomial.φ_def

added theorem SkewPolynomial.φ_iterate_apply

added def SkewPolynomial

Modified docs/references.bib