feat: port Algebra.GroupPower.Ring (#979)

Mathlib SHA: fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: joelriou

Mathlib.lean

@@ -25,6 +25,7 @@ import Mathlib.Algebra.Group.WithOne.Units
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.GroupPower.Identities
 import Mathlib.Algebra.GroupPower.Lemmas
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Defs

Mathlib/Algebra/GroupPower/Ring.lean

@@ -0,0 +1,280 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Robert Y. Lewis
+Ported by: Joël Riou
+-/
+
+import Mathlib.Algebra.GroupPower.Basic
+import Mathlib.Algebra.GroupWithZero.Commute
+import Mathlib.Algebra.Hom.Ring
+import Mathlib.Algebra.Ring.Commute
+import Mathlib.Algebra.GroupWithZero.Divisibility
+import Mathlib.Algebra.Ring.Divisibility
+import Mathlib.Data.Nat.Order.Basic
+
+/-!
+# Power operations on monoids with zero, semirings, and rings
+
+This file provides additional lemmas about the natural power operator on rings and semirings.
+Further lemmas about ordered semirings and rings can be found in `Algebra.GroupPower.Lemmas`.
+
+-/
+
+variable {R S M : Type _}
+
+section MonoidWithZero
+
+variable [MonoidWithZero M]
+
+theorem zero_pow : ∀ {n : ℕ}, 0 < n → (0 : M) ^ n = 0
+  | n + 1, _ => by rw [pow_succ, zero_mul]
+
+@[simp]
+theorem zero_pow' : ∀ n : ℕ, n ≠ 0 → (0 : M) ^ n = 0
+  | 0, h => absurd rfl h
+  | k + 1, _ => by
+    rw [pow_succ]
+    exact zero_mul _
+
+theorem zero_pow_eq (n : ℕ) : (0 : M) ^ n = if n = 0 then 1 else 0 := by
+  split_ifs with h
+  · rw [h, pow_zero]
+  · rw [zero_pow (Nat.pos_of_ne_zero h)]
+
+theorem pow_eq_zero_of_le {x : M} {n m : ℕ} (hn : n ≤ m) (hx : x ^ n = 0) : x ^ m = 0 := by
+  rw [← tsub_add_cancel_of_le hn, pow_add, hx, mul_zero]
+
+theorem pow_eq_zero [NoZeroDivisors M] {x : M} {n : ℕ} (H : x ^ n = 0) : x = 0 := by
+  induction' n with n ih
+  · rw [pow_zero] at H
+    rw [← mul_one x, H, mul_zero]
+  · rw [pow_succ] at H
+    exact Or.casesOn (mul_eq_zero.1 H) id ih
+
+@[simp]
+theorem pow_eq_zero_iff [NoZeroDivisors M] {a : M} {n : ℕ} (hn : 0 < n) : a ^ n = 0 ↔ a = 0 := by
+  refine' ⟨pow_eq_zero, _⟩
+  rintro rfl
+  exact zero_pow hn
+
+theorem pow_eq_zero_iff' [NoZeroDivisors M] [Nontrivial M] {a : M} {n : ℕ} :
+    a ^ n = 0 ↔ a = 0 ∧ n ≠ 0 := by cases (zero_le n).eq_or_gt <;> simp [*, ne_of_gt]
+
+theorem pow_ne_zero_iff [NoZeroDivisors M] {a : M} {n : ℕ} (hn : 0 < n) : a ^ n ≠ 0 ↔ a ≠ 0 :=
+  (pow_eq_zero_iff hn).not
+
+theorem ne_zero_pow {a : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≠ 0 → a ≠ 0 := by
+  contrapose!
+  rintro rfl
+  exact zero_pow' n hn
+#align ne_zero_pow ne_zero_pow
+
+@[field_simps]
+theorem pow_ne_zero [NoZeroDivisors M] {a : M} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
+  mt pow_eq_zero h
+#align pow_ne_zero pow_ne_zero
+
+instance NeZero.pow [NoZeroDivisors M] {x : M} [NeZero x] {n : ℕ} : NeZero (x ^ n) :=
+  ⟨pow_ne_zero n NeZero.out⟩
+#align ne_zero.pow NeZero.pow
+
+theorem sq_eq_zero_iff [NoZeroDivisors M] {a : M} : a ^ 2 = 0 ↔ a = 0 :=
+  pow_eq_zero_iff two_pos
+#align sq_eq_zero_iff sq_eq_zero_iff
+
+@[simp]
+theorem zero_pow_eq_zero [Nontrivial M] {n : ℕ} : (0 : M) ^ n = 0 ↔ 0 < n := by
+  constructor <;> intro h
+  · rw [pos_iff_ne_zero]
+    rintro rfl
+    simp at h
+  · exact zero_pow' n h.ne.symm
+
+theorem Ring.inverse_pow (r : M) : ∀ n : ℕ, Ring.inverse r ^ n = Ring.inverse (r ^ n)
+  | 0 => by rw [pow_zero, pow_zero, Ring.inverse_one]
+  | n + 1 => by
+    rw [pow_succ, pow_succ', Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
+      Ring.inverse_pow r n]
+
+end MonoidWithZero
+
+section CommMonoidWithZero
+
+variable [CommMonoidWithZero M] {n : ℕ} (hn : 0 < n)
+
+/-- We define `x ↦ x^n` (for positive `n : ℕ`) as a `monoid_with_zero_hom` -/
+def powMonoidWithZeroHom : M →*₀ M :=
+  { powMonoidHom n with map_zero' := zero_pow hn }
+
+@[simp]
+theorem coe_powMonoidWithZeroHom : (powMonoidWithZeroHom hn : M → M) = fun x ↦ (x^n : M) := rfl
+#align coe_pow_monoid_with_zero_hom coe_powMonoidWithZeroHom
+
+@[simp]
+theorem powMonoidWithZeroHom_apply (a : M) : powMonoidWithZeroHom hn a = a ^ n :=
+  rfl
+#align pow_monoid_with_zero_hom_apply powMonoidWithZeroHom_apply
+
+end CommMonoidWithZero
+
+theorem pow_dvd_pow_iff [CancelCommMonoidWithZero R] {x : R} {n m : ℕ} (h0 : x ≠ 0)
+    (h1 : ¬IsUnit x) : x ^ n ∣ x ^ m ↔ n ≤ m := by
+  constructor
+  · intro h
+    rw [← not_lt]
+    intro hmn
+    apply h1
+    have : x ^ m * x ∣ x ^ m * 1 := by
+      rw [← pow_succ', mul_one]
+      exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
+    rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
+    apply pow_ne_zero m h0
+  · apply pow_dvd_pow
+
+section Semiring
+
+variable [Semiring R] [Semiring S]
+
+protected theorem RingHom.map_pow (f : R →+* S) (a) : ∀ n : ℕ, f (a ^ n) = f a ^ n :=
+  map_pow f a
+#align ring_hom.map_pow RingHom.map_pow
+
+theorem min_pow_dvd_add {n m : ℕ} {a b c : R} (ha : c ^ n ∣ a) (hb : c ^ m ∣ b) :
+    c ^ min n m ∣ a + b := by
+  replace ha := (pow_dvd_pow c (min_le_left n m)).trans ha
+  replace hb := (pow_dvd_pow c (min_le_right n m)).trans hb
+  exact dvd_add ha hb
+
+end Semiring
+
+section CommSemiring
+
+variable [CommSemiring R]
+
+theorem add_sq (a b : R) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
+  simp only [sq, add_mul_self_eq]
+#align add_sq add_sq
+
+theorem add_sq' (a b : R) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b := by
+  rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
+#align add_sq' add_sq'
+
+alias add_sq ← add_pow_two
+
+end CommSemiring
+
+section HasDistribNeg
+
+variable [Monoid R] [HasDistribNeg R]
+
+variable (R)
+
+theorem neg_one_pow_eq_or : ∀ n : ℕ, (-1 : R) ^ n = 1 ∨ (-1 : R) ^ n = -1
+  | 0 => Or.inl (pow_zero _)
+  | n + 1 => (neg_one_pow_eq_or n).symm.imp
+    (fun h ↦ by rw [pow_succ, h, neg_one_mul, neg_neg])
+    (fun h ↦ by rw [pow_succ, h, mul_one])
+
+variable {R}
+
+theorem neg_pow (a : R) (n : ℕ) : (-a) ^ n = (-1) ^ n * a ^ n :=
+  neg_one_mul a ▸ (Commute.neg_one_left a).mul_pow n
+
+section
+set_option linter.deprecated false
+
+@[simp]
+theorem neg_pow_bit0 (a : R) (n : ℕ) : (-a) ^ bit0 n = a ^ bit0 n := by
+  rw [pow_bit0', neg_mul_neg, pow_bit0']
+#align neg_pow_bit0 neg_pow_bit0
+
+@[simp]
+theorem neg_pow_bit1 (a : R) (n : ℕ) : (-a) ^ bit1 n = -a ^ bit1 n := by
+  simp only [bit1, pow_succ, neg_pow_bit0, neg_mul_eq_neg_mul]
+#align neg_pow_bit1 neg_pow_bit1
+
+end
+
+@[simp]
+theorem neg_sq (a : R) : (-a) ^ 2 = a ^ 2 := by simp [sq]
+
+-- Porting note: removed the simp attribute to please the simpNF linter
+theorem neg_one_sq : (-1 : R) ^ 2 = 1 := by simp [neg_sq, one_pow]
+
+alias neg_sq ← neg_pow_two
+
+alias neg_one_sq ← neg_one_pow_two
+
+end HasDistribNeg
+
+section Ring
+
+variable [Ring R] {a b : R}
+
+protected theorem Commute.sq_sub_sq (h : Commute a b) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
+  rw [sq, sq, h.mul_self_sub_mul_self_eq]
+
+@[simp]
+theorem neg_one_pow_mul_eq_zero_iff {n : ℕ} {r : R} : (-1) ^ n * r = 0 ↔ r = 0 := by
+  rcases neg_one_pow_eq_or R n with h | h <;> simp [h]
+
+@[simp]
+theorem mul_neg_one_pow_eq_zero_iff {n : ℕ} {r : R} : r * (-1) ^ n = 0 ↔ r = 0 := by
+  rcases neg_one_pow_eq_or R n with h | h  <;> simp [h]
+
+variable [NoZeroDivisors R]
+
+protected theorem Commute.sq_eq_sq_iff_eq_or_eq_neg (h : Commute a b) :
+    a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
+  rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
+#align commute.sq_eq_sq_iff_eq_or_eq_neg Commute.sq_eq_sq_iff_eq_or_eq_neg
+
+@[simp]
+theorem sq_eq_one_iff : a ^ 2 = 1 ↔ a = 1 ∨ a = -1 := by
+  rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]
+#align sq_eq_one_iff sq_eq_one_iff
+
+theorem sq_ne_one_iff : a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1 :=
+  sq_eq_one_iff.not.trans not_or
+#align sq_ne_one_iff sq_ne_one_iff
+
+end Ring
+
+section CommRing
+
+variable [CommRing R]
+
+theorem sq_sub_sq (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b) :=
+  (Commute.all a b).sq_sub_sq
+
+alias sq_sub_sq ← pow_two_sub_pow_two
+
+theorem sub_sq (a b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 := by
+  rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
+
+alias sub_sq ← sub_pow_two
+
+theorem sub_sq' (a b : R) : (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b := by
+  rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
+
+variable [NoZeroDivisors R] {a b : R}
+
+theorem sq_eq_sq_iff_eq_or_eq_neg : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b :=
+  (Commute.all a b).sq_eq_sq_iff_eq_or_eq_neg
+
+theorem eq_or_eq_neg_of_sq_eq_sq (a b : R) : a ^ 2 = b ^ 2 → a = b ∨ a = -b :=
+  sq_eq_sq_iff_eq_or_eq_neg.1
+
+-- Copies of the above CommRing lemmas for `Units R`.
+namespace Units
+
+protected theorem sq_eq_sq_iff_eq_or_eq_neg {a b : Rˣ} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
+  simp_rw [ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg, iff_self]
+
+protected theorem eq_or_eq_neg_of_sq_eq_sq (a b : Rˣ) (h : a ^ 2 = b ^ 2) : a = b ∨ a = -b :=
+  Units.sq_eq_sq_iff_eq_or_eq_neg.1 h
+
+end Units
+
+end CommRing

Mathlib/Tactic/Positivity/Basic.lean

@@ -8,7 +8,7 @@ import Mathlib.Tactic.Positivity.Core
 import Mathlib.Tactic.Clear!
 import Mathlib.Logic.Nontrivial
 import Mathlib.Algebra.CovariantAndContravariant
-import Mathlib.Algebra.GroupPower.Basic
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Order.Ring.Lemmas
@@ -61,15 +61,6 @@ instance [StrictOrderedSemiring α] : OrderedMonoidWithZero α :=
 instance [StrictOrderedSemiring α] : MulPosStrictMono α :=
   ⟨fun ⟨_, ha⟩ _ _ h => StrictOrderedSemiring.mul_lt_mul_of_pos_right _ _ _ h ha⟩
 
-theorem pow_ne_zero [MonoidWithZero M] [NoZeroDivisors M] {a : M} (n : ℕ) (h : a ≠ 0) :
-    a ^ n ≠ 0 := by
-  refine mt (fun H => ?_) h
-  induction' n with n IH
-  · rw [pow_zero] at H
-    rw [←mul_one a, H, mul_zero]
-  · rw [pow_succ, mul_eq_zero] at H
-    exact H.casesOn id IH
-
 lemma mul_ne_zero_of_ne_zero_of_pos [Zero α] [Mul α] [PartialOrder α] [NoZeroDivisors α]
     {a b : α} (ha : a ≠ 0) (hb : 0 < b) : a * b ≠ 0 :=
   mul_ne_zero ha (ne_of_gt hb)