Commit 2025-05-07 20:43 9dbbedce

View on Github →

chore(Topology/Algebra/Order/Field): rename 2 lemmas (#24302)

Estimated changes

Modified Mathlib/Topology/Algebra/Order/Field.lean

added theorem tendsto_inv_atBot_nhdsLT_zero

deleted theorem tendsto_inv_atBot_zero'

added theorem tendsto_inv_nhdsLT_zero

deleted theorem tendsto_inv_zero_atBot