Commit 2024-02-09 19:37 77656757

View on Github →

feat: generalize ContinuousMultilinearLinearMap.mkPiField to mkPiRing (#9910) This matches the generality of the non-continuous versions. The norm_smulRight lemma is the only new result.

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

deleted theorem FormalMultilinearSeries.mkPiField_coeff_eq

added theorem FormalMultilinearSeries.mkPiRing_coeff_eq

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

deleted theorem ContinuousMultilinearMap.mkPiField_apply

deleted theorem ContinuousMultilinearMap.mkPiField_apply_one_eq_self

deleted theorem ContinuousMultilinearMap.mkPiField_eq_iff

deleted theorem ContinuousMultilinearMap.mkPiField_eq_zero_iff

deleted theorem ContinuousMultilinearMap.mkPiField_zero

added theorem ContinuousMultilinearMap.nnnorm_smulRight

deleted theorem ContinuousMultilinearMap.norm_mkPiField

added theorem ContinuousMultilinearMap.norm_mkPiRing

added theorem ContinuousMultilinearMap.norm_smulRight

Modified Mathlib/Analysis/NormedSpace/Spectrum.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

added theorem ContinuousMultilinearMap.mkPiRing_apply

added theorem ContinuousMultilinearMap.mkPiRing_apply_one_eq_self

added theorem ContinuousMultilinearMap.mkPiRing_eq_iff

added theorem ContinuousMultilinearMap.mkPiRing_eq_zero_iff

added theorem ContinuousMultilinearMap.mkPiRing_zero