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.
chore: avoid ≥ in ofScalars_radius_ge_inv_of_tendsto (#31881)
I stumbled into this use of ≥, which goes against mathlib conventions.