Theorem zpow_le_of_le
Modification history
2025-04-11 00:24
Mathlib/Algebra/Order/Field/Power.lean
chore: delete >6 month old deprecations (2024-10 01-10) (#23928) …
Deleted zpow_le_of_leView on Github →2024-10-11 15:01
Mathlib/Algebra/Order/Field/Power.lean
chore: generalise `zpow` lemmas from `LinearOrderedSemifield` to `GroupWithZero` (#17539)
Modified zpow_le_of_leView on Github →