Commit 2025-06-04 07:53 9ac601a0

View on Github →

feat: the Gauss norm of power series and polynomials (#24940) We introduce Gauss norms for power series and polynomials. Zulip discussion here

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/GaussNorm.lean

added theorem Polynomial.exists_eq_gaussNorm

added def Polynomial.gaussNorm

added theorem Polynomial.gaussNorm_C

added theorem Polynomial.gaussNorm_coe_powerSeries

added theorem Polynomial.gaussNorm_eq_zero_iff

added theorem Polynomial.gaussNorm_monomial

added theorem Polynomial.gaussNorm_nonneg

added theorem Polynomial.gaussNorm_zero

added theorem Polynomial.le_gaussNorm

added theorem PowerSeries.gaussNorm_C

added theorem PowerSeries.gaussNorm_monomial

Created Mathlib/RingTheory/PowerSeries/GaussNorm.lean

added theorem PowerSeries.gaussNorm_eq_zero_iff

added theorem PowerSeries.gaussNorm_nonneg

added theorem PowerSeries.gaussNorm_zero

added theorem PowerSeries.le_gaussNorm