Commit 2023-02-22 02:44 af82934b

View on Github →

feat: Port Topology.Algebra.Order.Group (#2426) Rename only.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Order/Group.lean

added theorem continuous_abs

added theorem tendsto_abs_nhdsWithin_zero

added theorem tendsto_zero_iff_abs_tendsto_zero