Commit 2026-04-17 15:52 f99e871a

View on Github →

refactor: PowerSeries.gaussNorm (#38074) We refactor the definition of the gauss norm on power series to an abbrev of the gauss norm on multivariate power series, and remove the use of Funlike.

Estimated changes