Commit 2023-06-15 04:33 dd52d5fb

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Order/AbsoluteValue.lean

modified def AbsoluteValue.Simps.apply

modified theorem AbsoluteValue.coe_toMulHom