Commit 2026-06-01 13:21 c5f6a0fe

View on Github →

feat(Algebra/SkewPolynomial/Basic): add API (#38619) We add API for SkewPolynomial, including monomial, coeff, C and X. Co-authored by: @xgenereux.

Estimated changes

added def SkewPolynomial.C
added theorem SkewPolynomial.C_0
added theorem SkewPolynomial.C_1
added theorem SkewPolynomial.C_add
added theorem SkewPolynomial.C_inj
added theorem SkewPolynomial.C_mul
added theorem SkewPolynomial.C_pow
added def SkewPolynomial.X
added theorem SkewPolynomial.X_mul
added theorem SkewPolynomial.coeff_C
added theorem SkewPolynomial.coeff_X
added theorem SkewPolynomial.ext
added theorem SkewPolynomial.ext_iff
modified theorem SkewPolynomial.monomial_add
modified theorem SkewPolynomial.monomial_def
added theorem SkewPolynomial.mul_def
added theorem SkewPolynomial.sum_def