Commit 2025-09-15 08:45 f0533f4b

View on Github →

chore: fix a few typos (#29470) chore: fix some typos and add deprecations accordingly

Estimated changes

Modified Mathlib/Algebra/Group/Action/Faithful.lean

Modified Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

added theorem ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear

deleted theorem ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

Modified Mathlib/Analysis/Polynomial/Factorization.lean