Theorem zpow_left_injOn₀

Modification history

2026-01-28 08:39
Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean
feat(Algebra/Order): injectivity of `zpow` in its left argument (#23177)
Added zpow_left_injOn₀View on Github →