Commit 2025-11-24 14:10 4dba3bd1

View on Github →

chore: avoid ≥ in ofScalars_radius_ge_inv_of_tendsto (#31881) I stumbled into this use of ≥, which goes against mathlib conventions.

Estimated changes

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Analytic/OfScalars.lean

added theorem FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto

deleted theorem FormalMultilinearSeries.ofScalars_radius_ge_inv_of_tendsto