Theorem FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2

Modification history

2024-09-28 07:48
Mathlib/Analysis/Analytic/Inverse.lean
feat: the inverse of an analytic partial homeo is also analytic (#17170) …
Modified FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2View on Github →
2023-07-13 04:40
Mathlib/Analysis/Analytic/Inverse.lean
feat: port Analysis.Analytic.Inverse (#5032)
Added FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2View on Github →