Commit 2025-12-26 12:38 9165b4d3
View on Github →feat: zpow left ₀ lemmas (#33051)
Add the •₀ version of : zpow_le_zpow_left, zpow_lt_zpow_left, zpow_le_zpow_iff_left and zpow_lt_zpow_iff_left.
I also moved zpow_left_strictMonoOn₀ to be in the new section I created, avoiding the use of omit.