Theorem mabs_pow

Modification history

2025-03-15 13:13

Mathlib/Algebra/Order/Group/Abs.lean

chore(Order/Group/Abs): use `@[to_additive]` (#22468)

Modified mabs_pow View on Github →

2024-01-18 17:23

Mathlib/Algebra/Order/Group/Abs.lean

chore: Move order lemmas about `zpow` (#9805) …

Added mabs_pow View on Github →