Def AbsoluteValue.Simps.apply

Modification history

2023-06-15 04:33

Mathlib/Algebra/Order/AbsoluteValue.lean

feat: port Algebra.Order.AbsoluteValue again (#3448)

Modified AbsoluteValue.Simps.apply View on Github →

2023-02-28 04:45

Mathlib/Algebra/Order/AbsoluteValue.lean

feat: define `UniformSpace.ofFun` (#2511) …

Added AbsoluteValue.Simps.apply View on Github →