Theorem mabs_mul_eq_mul_mabs_iff

Modification history

2025-03-15 13:13
Mathlib/Algebra/Order/Group/Abs.lean
chore(Order/Group/Abs): use `@[to_additive]` (#22468)
Modified mabs_mul_eq_mul_mabs_iffView on Github →
2024-01-18 17:23
Mathlib/Algebra/Order/Group/Abs.lean
chore: Move order lemmas about `zpow` (#9805) …
Added mabs_mul_eq_mul_mabs_iffView on Github →