Theorem FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto

Modification history

2025-11-24 14:10
Mathlib/Analysis/Analytic/OfScalars.lean
chore: avoid `≥` in `ofScalars_radius_ge_inv_of_tendsto` (#31881) …
Added FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendstoView on Github →