Commit 2023-07-13 04:40 cf365f06

View on Github →

feat: port Analysis.Analytic.Inverse (#5032)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Analytic/Inverse.lean

added theorem FormalMultilinearSeries.comp_rightInv

added theorem FormalMultilinearSeries.comp_rightInv_aux1

added theorem FormalMultilinearSeries.comp_rightInv_aux2

added theorem FormalMultilinearSeries.leftInv_coeff_one

added theorem FormalMultilinearSeries.leftInv_coeff_zero

added theorem FormalMultilinearSeries.leftInv_comp

added theorem FormalMultilinearSeries.leftInv_eq_rightInv

added theorem FormalMultilinearSeries.leftInv_removeZero

added theorem FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos

added theorem FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2

added theorem FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1

added theorem FormalMultilinearSeries.rightInv_coeff

added theorem FormalMultilinearSeries.rightInv_coeff_one

added theorem FormalMultilinearSeries.rightInv_coeff_zero

added theorem FormalMultilinearSeries.rightInv_removeZero