feat: a ^ n = 1 ↔ n = 0 and similar (#17745)

This PR adds a few lemmas about GroupsWithZero, more precisely:

- the lemmas `zero_pow_eq_one₀`, `zero_zpow_eq_one₀` to Algebra.GroupWithZero.Basic and 

- `zpow_le_zpow_iff_right_of_lt_one₀`, `zpow_lt_zpow_iff_right_of_lt_one₀` and `zpow_eq_one_iff_right₀` to Algebra.Order.GroupWithZero.Unbundled.

Used in project Formalization of the Bruhat-Tits Tree.
Co-authored-by: Christian Merten <[email protected]>



Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: judithludwig <[email protected]>

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -146,6 +146,9 @@ lemma zero_pow_eq (n : ℕ) : (0 : M₀) ^ n = if n = 0 then 1 else 0 := by
   · rw [h, pow_zero]
   · rw [zero_pow h]
 
+lemma zero_pow_eq_one₀ [Nontrivial M₀] : (0 : M₀) ^ n = 1 ↔ n = 0 := by
+  rw [zero_pow_eq, one_ne_zero.ite_eq_left_iff]
+
 lemma pow_eq_zero_of_le : ∀ {m n} (_ : m ≤ n) (_ : a ^ m = 0), a ^ n = 0
   | _, _, Nat.le.refl, ha => ha
   | _, _, Nat.le.step hmn, ha => by rw [pow_succ, pow_eq_zero_of_le hmn ha, zero_mul]
@@ -389,6 +392,9 @@ lemma zero_zpow_eq (n : ℤ) : (0 : G₀) ^ n = if n = 0 then 1 else 0 := by
   · rw [h, zpow_zero]
   · rw [zero_zpow _ h]
 
+lemma zero_zpow_eq_one₀ {n : ℤ} : (0 : G₀) ^ n = 1 ↔ n = 0 := by
+  rw [zero_zpow_eq, one_ne_zero.ite_eq_left_iff]
+
 lemma zpow_add_one₀ (ha : a ≠ 0) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
   | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_natCast, pow_succ]
   | .negSucc 0 => by erw [zpow_zero, zpow_negSucc, pow_one, inv_mul_cancel₀ ha]

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

@@ -1407,8 +1407,8 @@ lemma zpow_lt_zpow_right₀ (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n :=
   zpow_right_strictMono₀ ha hmn
 
 @[gcongr]
-lemma zpow_lt_zpow_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hmn : m ≤ n) : a ^ n ≤ a ^ m :=
-  zpow_right_anti₀ ha₀ ha₁ hmn
+lemma zpow_lt_zpow_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m :=
+  zpow_right_strictAnti₀ ha₀ ha₁ hmn
 
 lemma one_lt_zpow₀ (ha : 1 < a) (hn : 0 < n) : 1 < a ^ n := by
   simpa using zpow_right_strictMono₀ ha hn
@@ -1428,6 +1428,12 @@ lemma one_lt_zpow_of_neg₀ (ha₀ : 0 < a) (ha₁ : a < 1) (hn : n < 0) : 1 < a
 @[simp] lemma zpow_lt_zpow_iff_right₀ (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
   (zpow_right_strictMono₀ ha).lt_iff_lt
 
+lemma zpow_le_zpow_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) :
+    a ^ m ≤ a ^ n ↔ n ≤ m := (zpow_right_strictAnti₀ ha₀ ha₁).le_iff_le
+
+lemma zpow_lt_zpow_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) :
+    a ^ m < a ^ n ↔ n < m := (zpow_right_strictAnti₀ ha₀ ha₁).lt_iff_lt
+
 end PosMulStrictMono
 
 section MulPosStrictMono
@@ -1512,6 +1518,11 @@ lemma zpow_right_injective₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective fun
 @[simp] lemma zpow_right_inj₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n :=
   (zpow_right_injective₀ ha₀ ha₁).eq_iff
 
+lemma zpow_eq_one_iff_right₀ (ha₀ : 0 ≤ a) (ha₁ : a ≠ 1) {n : ℤ} : a ^ n = 1 ↔ n = 0 := by
+  obtain rfl | ha₀ := ha₀.eq_or_lt
+  · exact zero_zpow_eq_one₀
+  simpa using zpow_right_inj₀ ha₀ ha₁ (n := 0)
+
 end GroupWithZero.LinearOrder
 
 section CommSemigroupHasZero