Theorem continuous_abs

Modification history

2025-03-21 06:09

Mathlib/Topology/Algebra/Order/Group.lean

chore(Topology/Order): use @[to_additive] (#22463)

Deleted continuous_abs View on Github →

2023-02-22 02:44

Mathlib/Topology/Algebra/Order/Group.lean

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

Added continuous_abs View on Github →