Commit 2023-05-23 11:05 51c31d5b

View on Github →

feat: port Analysis.Calculus.FormalMultilinearSeries (#4114)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

added def ContinuousLinearMap.compFormalMultilinearSeries

added theorem ContinuousLinearMap.compFormalMultilinearSeries_apply'

added theorem ContinuousLinearMap.compFormalMultilinearSeries_apply

added theorem FormalMultilinearSeries.apply_eq_pow_smul_coeff

added theorem FormalMultilinearSeries.apply_eq_prod_smul_coeff

added theorem FormalMultilinearSeries.apply_eq_zero_of_lt_order

added theorem FormalMultilinearSeries.apply_order_ne_zero'

added theorem FormalMultilinearSeries.apply_order_ne_zero

added def FormalMultilinearSeries.coeff

added theorem FormalMultilinearSeries.coeff_eq_zero

added theorem FormalMultilinearSeries.coeff_fslope

added theorem FormalMultilinearSeries.coeff_iterate_fslope

added def FormalMultilinearSeries.compContinuousLinearMap

added theorem FormalMultilinearSeries.compContinuousLinearMap_apply

added theorem FormalMultilinearSeries.congr

added theorem FormalMultilinearSeries.mkPiField_coeff_eq

added theorem FormalMultilinearSeries.ne_zero_of_order_ne_zero

added theorem FormalMultilinearSeries.norm_apply_eq_norm_coef

added theorem FormalMultilinearSeries.order_eq_find'

added theorem FormalMultilinearSeries.order_eq_find

added theorem FormalMultilinearSeries.order_eq_zero_iff'

added theorem FormalMultilinearSeries.order_eq_zero_iff

added theorem FormalMultilinearSeries.order_zero

added def FormalMultilinearSeries.removeZero

added theorem FormalMultilinearSeries.removeZero_coeff_succ

added theorem FormalMultilinearSeries.removeZero_coeff_zero

added theorem FormalMultilinearSeries.removeZero_of_pos

added def FormalMultilinearSeries.shift

added def FormalMultilinearSeries.unshift

added def FormalMultilinearSeries

added def constFormalMultilinearSeries

added theorem constFormalMultilinearSeries_apply

added theorem zero_apply