Theorem FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1

Modification history

2023-07-13 04:40
Mathlib/Analysis/Analytic/Inverse.lean
feat: port Analysis.Analytic.Inverse (#5032)
Added FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1View on Github →