Commit 2024-01-06 11:11 87ffb361

View on Github →

chore: move a few results from Archive.Hairer into mathlib (#9315)

Estimated changes

Modified Archive/Hairer.lean

deleted theorem MvPolynomial.continuous_eval

modified theorem SmoothSupportedOn.integrable_eval_mul

Modified Mathlib.lean

Modified Mathlib/Data/Set/Finite.lean

added theorem Set.Finite.pi'

modified theorem Set.Finite.pi

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

Created Mathlib/Topology/Algebra/MvPolynomial.lean

added theorem MvPolynomial.continuous_eval