Trigger CI for leanprover/lean4#3040

Mathlib.lean

@@ -2197,6 +2197,7 @@ import Mathlib.GroupTheory.GroupAction.Option
 import Mathlib.GroupTheory.GroupAction.Pi
 import Mathlib.GroupTheory.GroupAction.Prod
 import Mathlib.GroupTheory.GroupAction.Quotient
+import Mathlib.GroupTheory.GroupAction.Ring
 import Mathlib.GroupTheory.GroupAction.Sigma
 import Mathlib.GroupTheory.GroupAction.SubMulAction
 import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
@@ -2974,6 +2975,7 @@ import Mathlib.Probability.ConditionalExpectation
 import Mathlib.Probability.ConditionalProbability
 import Mathlib.Probability.Density
 import Mathlib.Probability.Distributions.Exponential
+import Mathlib.Probability.Distributions.Gamma
 import Mathlib.Probability.Distributions.Gaussian
 import Mathlib.Probability.IdentDistrib
 import Mathlib.Probability.Independence.Basic

Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean

@@ -3,11 +3,10 @@ Copyright (c) 2023 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
-
-import Mathlib.Algebra.Algebra.NonUnitalSubalgebra
-import Mathlib.Algebra.Star.Subalgebra
 import Mathlib.Algebra.Algebra.Unitization
 import Mathlib.Algebra.Star.NonUnitalSubalgebra
+import Mathlib.Algebra.Star.Subalgebra
+import Mathlib.GroupTheory.GroupAction.Ring
 
 /-!
 # Relating unital and non-unital substructures

Mathlib/Algebra/Associated.lean

@@ -3,8 +3,6 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
 -/
-import Mathlib.Algebra.Divisibility.Basic
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.Parity
 
 #align_import algebra.associated from "leanprover-community/mathlib"@"2f3994e1b117b1e1da49bcfb67334f33460c3ce4"
@@ -306,7 +304,7 @@ variable [CommMonoid α] {a : α}
 theorem Irreducible.not_square (ha : Irreducible a) : ¬IsSquare a := by
   rw [isSquare_iff_exists_sq]
   rintro ⟨b, rfl⟩
-  exact not_irreducible_pow one_lt_two.ne' ha
+  exact not_irreducible_pow (by decide) ha
 #align irreducible.not_square Irreducible.not_square
 
 theorem IsSquare.not_irreducible (ha : IsSquare a) : ¬Irreducible a := fun h => h.not_square ha

Mathlib/Algebra/Group/Commute/Basic.lean

@@ -58,4 +58,38 @@ protected theorem div_div_div_comm (hbc : Commute b c) (hbd : Commute b⁻¹ d)
 
 end DivisionMonoid
 
+section Group
+variable [Group G] {a b : G}
+
+@[to_additive (attr := simp)]
+lemma inv_left_iff : Commute a⁻¹ b ↔ Commute a b := SemiconjBy.inv_symm_left_iff
+#align commute.inv_left_iff Commute.inv_left_iff
+#align add_commute.neg_left_iff AddCommute.neg_left_iff
+
+@[to_additive] alias ⟨_, inv_left⟩ := inv_left_iff
+#align commute.inv_left Commute.inv_left
+#align add_commute.neg_left AddCommute.neg_left
+
+@[to_additive (attr := simp)]
+lemma inv_right_iff : Commute a b⁻¹ ↔ Commute a b := SemiconjBy.inv_right_iff
+#align commute.inv_right_iff Commute.inv_right_iff
+#align add_commute.neg_right_iff AddCommute.neg_right_iff
+
+@[to_additive] alias ⟨_, inv_right⟩ := inv_right_iff
+#align commute.inv_right Commute.inv_right
+#align add_commute.neg_right AddCommute.neg_right
+
+@[to_additive]
+protected lemma inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b := by
+  rw [h.inv_left.eq, inv_mul_cancel_right]
+#align commute.inv_mul_cancel Commute.inv_mul_cancel
+#align add_commute.neg_add_cancel AddCommute.neg_add_cancel
+
+@[to_additive]
+lemma inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by
+  rw [← mul_assoc, h.inv_mul_cancel]
+#align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc
+#align add_commute.neg_add_cancel_assoc AddCommute.neg_add_cancel_assoc
+
+end Group
 end Commute

Mathlib/Algebra/Group/Commute/Units.lean

@@ -99,65 +99,4 @@ theorem _root_.isUnit_mul_self_iff : IsUnit (a * a) ↔ IsUnit a :=
 #align is_add_unit_add_self_iff isAddUnit_add_self_iff
 
 end Monoid
-
-section Group
-
-variable [Group G] {a b : G}
-
-@[to_additive]
-theorem inv_right : Commute a b → Commute a b⁻¹ :=
-  SemiconjBy.inv_right
-#align commute.inv_right Commute.inv_right
-#align add_commute.neg_right AddCommute.neg_right
-
-@[to_additive (attr := simp)]
-theorem inv_right_iff : Commute a b⁻¹ ↔ Commute a b :=
-  SemiconjBy.inv_right_iff
-#align commute.inv_right_iff Commute.inv_right_iff
-#align add_commute.neg_right_iff AddCommute.neg_right_iff
-
-@[to_additive]
-theorem inv_left : Commute a b → Commute a⁻¹ b :=
-  SemiconjBy.inv_symm_left
-#align commute.inv_left Commute.inv_left
-#align add_commute.neg_left AddCommute.neg_left
-
-@[to_additive (attr := simp)]
-theorem inv_left_iff : Commute a⁻¹ b ↔ Commute a b :=
-  SemiconjBy.inv_symm_left_iff
-#align commute.inv_left_iff Commute.inv_left_iff
-#align add_commute.neg_left_iff AddCommute.neg_left_iff
-
-@[to_additive]
-protected theorem inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b := by
-  rw [h.inv_left.eq, inv_mul_cancel_right]
-#align commute.inv_mul_cancel Commute.inv_mul_cancel
-#align add_commute.neg_add_cancel AddCommute.neg_add_cancel
-
-@[to_additive]
-theorem inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by
-  rw [← mul_assoc, h.inv_mul_cancel]
-#align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc
-#align add_commute.neg_add_cancel_assoc AddCommute.neg_add_cancel_assoc
-
-end Group
-
 end Commute
-
-section CommGroup
-
-variable [CommGroup G] (a b : G)
-
-@[to_additive (attr := simp)]
-theorem inv_mul_cancel_comm : a⁻¹ * b * a = b :=
-  (Commute.all a b).inv_mul_cancel
-#align inv_mul_cancel_comm inv_mul_cancel_comm
-#align neg_add_cancel_comm neg_add_cancel_comm
-
-@[to_additive (attr := simp)]
-theorem inv_mul_cancel_comm_assoc : a⁻¹ * (b * a) = b :=
-  (Commute.all a b).inv_mul_cancel_assoc
-#align inv_mul_cancel_comm_assoc inv_mul_cancel_comm_assoc
-#align neg_add_cancel_comm_assoc neg_add_cancel_comm_assoc
-
-end CommGroup

Mathlib/Algebra/Group/Defs.lean

@@ -998,6 +998,10 @@ theorem zpow_ofNat (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
 #align zpow_of_nat zpow_ofNat
 #align of_nat_zsmul ofNat_zsmul
 
+@[to_additive (attr := simp, norm_cast) coe_nat_zsmul]
+lemma zpow_coe_nat (a : G) (n : ℕ) : a ^ (Nat.cast n : ℤ) = a ^ n := zpow_ofNat ..
+#align coe_nat_zsmul coe_nat_zsmul
+
 theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ := by
   rw [← zpow_ofNat]
   exact DivInvMonoid.zpow_neg' n a
@@ -1263,6 +1267,16 @@ instance (priority := 100) CommGroup.toCancelCommMonoid : CancelCommMonoid G :=
 instance (priority := 100) CommGroup.toDivisionCommMonoid : DivisionCommMonoid G :=
   { ‹CommGroup G›, Group.toDivisionMonoid with }
 
+@[to_additive (attr := simp)] lemma inv_mul_cancel_comm (a b : G) : a⁻¹ * b * a = b := by
+  rw [mul_comm, mul_inv_cancel_left]
+#align inv_mul_cancel_comm inv_mul_cancel_comm
+#align neg_add_cancel_comm neg_add_cancel_comm
+
+@[to_additive (attr := simp)] lemma inv_mul_cancel_comm_assoc (a b : G) : a⁻¹ * (b * a) = b := by
+  rw [mul_comm, mul_inv_cancel_right]
+#align inv_mul_cancel_comm_assoc inv_mul_cancel_comm_assoc
+#align neg_add_cancel_comm_assoc neg_add_cancel_comm_assoc
+
 end CommGroup
 
 /-! We initialize all projections for `@[simps]` here, so that we don't have to do it in later

Mathlib/Algebra/Group/Semiconj/Basic.lean

@@ -9,29 +9,47 @@ import Mathlib.Algebra.Group.Basic
 #align_import algebra.group.semiconj from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
 
 /-!
-# Lemmas about semiconjugate elements of a semigroup
+# Lemmas about semiconjugate elements of a group
 
 -/
 
 namespace SemiconjBy
+variable {G : Type*}
 
 section DivisionMonoid
-
-variable {G : Type*} [DivisionMonoid G] {a x y : G}
+variable [DivisionMonoid G] {a x y : G}
 
 @[to_additive (attr := simp)]
-theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x :=
-  inv_involutive.injective.eq_iff.symm.trans <| by
-    rw [mul_inv_rev, mul_inv_rev, inv_inv, inv_inv, inv_inv, eq_comm, SemiconjBy]
+theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x := by
+  simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]
 #align semiconj_by.inv_inv_symm_iff SemiconjBy.inv_inv_symm_iff
 #align add_semiconj_by.neg_neg_symm_iff AddSemiconjBy.neg_neg_symm_iff
 
-@[to_additive]
-theorem inv_inv_symm : SemiconjBy a x y → SemiconjBy a⁻¹ y⁻¹ x⁻¹ :=
-  inv_inv_symm_iff.2
+@[to_additive] alias ⟨_, inv_inv_symm⟩ := inv_inv_symm_iff
 #align semiconj_by.inv_inv_symm SemiconjBy.inv_inv_symm
 #align add_semiconj_by.neg_neg_symm AddSemiconjBy.neg_neg_symm
 
 end DivisionMonoid
 
+section Group
+variable [Group G] {a x y : G}
+
+@[to_additive (attr := simp)] lemma inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y := by
+  simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]
+#align semiconj_by.inv_symm_left_iff SemiconjBy.inv_symm_left_iff
+#align add_semiconj_by.neg_symm_left_iff AddSemiconjBy.neg_symm_left_iff
+
+@[to_additive] alias ⟨_, inv_symm_left⟩ := inv_symm_left_iff
+#align semiconj_by.inv_symm_left SemiconjBy.inv_symm_left
+#align add_semiconj_by.neg_symm_left AddSemiconjBy.neg_symm_left
+
+@[to_additive (attr := simp)] lemma inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y := by
+  rw [← inv_symm_left_iff, inv_inv_symm_iff]
+#align add_semiconj_by.neg_right_iff AddSemiconjBy.neg_right_iff
+
+@[to_additive] alias ⟨_, inv_right⟩ := inv_right_iff
+#align semiconj_by.inv_right SemiconjBy.inv_right
+#align add_semiconj_by.neg_right AddSemiconjBy.neg_right
+
+end Group
 end SemiconjBy

Mathlib/Algebra/Group/Semiconj/Units.lean

@@ -88,38 +88,6 @@ theorem units_val_iff {a x y : Mˣ} : SemiconjBy (a : M) x y ↔ SemiconjBy a x
 #align add_semiconj_by.add_units_coe_iff AddSemiconjBy.addUnits_val_iff
 
 end Monoid
-
-section Group
-
-variable [Group G] {a x y : G}
-
-@[to_additive (attr := simp)]
-theorem inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y :=
-  @units_inv_right_iff G _ a ⟨x, x⁻¹, mul_inv_self x, inv_mul_self x⟩
-    ⟨y, y⁻¹, mul_inv_self y, inv_mul_self y⟩
-#align semiconj_by.inv_right_iff SemiconjBy.inv_right_iff
-#align add_semiconj_by.neg_right_iff AddSemiconjBy.neg_right_iff
-
-@[to_additive]
-theorem inv_right : SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹ :=
-  inv_right_iff.2
-#align semiconj_by.inv_right SemiconjBy.inv_right
-#align add_semiconj_by.neg_right AddSemiconjBy.neg_right
-
-@[to_additive (attr := simp)]
-theorem inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y :=
-  @units_inv_symm_left_iff G _ ⟨a, a⁻¹, mul_inv_self a, inv_mul_self a⟩ _ _
-#align semiconj_by.inv_symm_left_iff SemiconjBy.inv_symm_left_iff
-#align add_semiconj_by.neg_symm_left_iff AddSemiconjBy.neg_symm_left_iff
-
-@[to_additive]
-theorem inv_symm_left : SemiconjBy a x y → SemiconjBy a⁻¹ y x :=
-  inv_symm_left_iff.2
-#align semiconj_by.inv_symm_left SemiconjBy.inv_symm_left
-#align add_semiconj_by.neg_symm_left AddSemiconjBy.neg_symm_left
-
-end Group
-
 end SemiconjBy
 
 /-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/

Mathlib/Algebra/GroupPower/Basic.lean

@@ -3,9 +3,9 @@ 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
 -/
-import Mathlib.Algebra.Group.Commute.Units
+import Mathlib.Algebra.Group.Commute.Basic
 import Mathlib.Algebra.GroupWithZero.Defs
-import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Common
 
 #align_import algebra.group_power.basic from "leanprover-community/mathlib"@"9b2660e1b25419042c8da10bf411aa3c67f14383"
 

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -10,6 +10,7 @@ import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Data.Nat.Pow
 import Mathlib.Data.Int.Cast.Lemmas
 import Mathlib.Algebra.Group.Opposite
+import Mathlib.GroupTheory.GroupAction.Ring
 
 #align_import algebra.group_power.lemmas from "leanprover-community/mathlib"@"a07d750983b94c530ab69a726862c2ab6802b38c"
 
@@ -511,24 +512,6 @@ theorem nsmul_eq_mul [NonAssocSemiring R] (n : ℕ) (a : R) : n • a = n * a :=
 #align nsmul_eq_mul nsmul_eq_mulₓ
 -- typeclasses do not match up exactly.
 
-/-- Note that `AddCommMonoid.nat_smulCommClass` requires stronger assumptions on `R`. -/
-instance NonUnitalNonAssocSemiring.nat_smulCommClass [NonUnitalNonAssocSemiring R] :
-    SMulCommClass ℕ R R :=
-  ⟨fun n x y => by
-    induction' n with n ih
-    · simp [zero_nsmul]
-    · simp_rw [succ_nsmul, smul_eq_mul, mul_add, ← smul_eq_mul, ih]⟩
-#align non_unital_non_assoc_semiring.nat_smul_comm_class NonUnitalNonAssocSemiring.nat_smulCommClass
-
-/-- Note that `AddCommMonoid.nat_isScalarTower` requires stronger assumptions on `R`. -/
-instance NonUnitalNonAssocSemiring.nat_isScalarTower [NonUnitalNonAssocSemiring R] :
-    IsScalarTower ℕ R R :=
-  ⟨fun n x y => by
-    induction' n with n ih
-    · simp [zero_nsmul]
-    · simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]⟩
-#align non_unital_non_assoc_semiring.nat_is_scalar_tower NonUnitalNonAssocSemiring.nat_isScalarTower
-
 @[simp, norm_cast]
 theorem Nat.cast_pow [Semiring R] (n m : ℕ) : (↑(n ^ m) : R) = (↑n : R) ^ m := by
   induction' m with m ih
@@ -596,24 +579,6 @@ theorem zsmul_eq_mul' [Ring R] (a : R) (n : ℤ) : n • a = a * n := by
   rw [zsmul_eq_mul, (n.cast_commute a).eq]
 #align zsmul_eq_mul' zsmul_eq_mul'
 
-/-- Note that `AddCommGroup.int_smulCommClass` requires stronger assumptions on `R`. -/
-instance NonUnitalNonAssocRing.int_smulCommClass [NonUnitalNonAssocRing R] :
-    SMulCommClass ℤ R R :=
-  ⟨fun n x y =>
-    match n with
-    | (n : ℕ) => by simp_rw [coe_nat_zsmul, smul_comm]
-    | -[n+1] => by simp_rw [negSucc_zsmul, smul_eq_mul, mul_neg, mul_smul_comm]⟩
-#align non_unital_non_assoc_ring.int_smul_comm_class NonUnitalNonAssocRing.int_smulCommClass
-
-/-- Note that `AddCommGroup.int_isScalarTower` requires stronger assumptions on `R`. -/
-instance NonUnitalNonAssocRing.int_isScalarTower [NonUnitalNonAssocRing R] :
-    IsScalarTower ℤ R R :=
-  ⟨fun n x y =>
-    match n with
-    | (n : ℕ) => by simp_rw [coe_nat_zsmul, smul_assoc]
-    | -[n+1] => by simp_rw [negSucc_zsmul, smul_eq_mul, neg_mul, smul_mul_assoc]⟩
-#align non_unital_non_assoc_ring.int_is_scalar_tower NonUnitalNonAssocRing.int_isScalarTower
-
 theorem zsmul_int_int (a b : ℤ) : a • b = a * b := by simp
 #align zsmul_int_int zsmul_int_int
 

Mathlib/Algebra/GroupPower/NegOnePow.lean

@@ -86,4 +86,13 @@ lemma negOnePow_eq_iff (n₁ n₂ : ℤ) :
       Int.even_iff_not_odd, Int.even_iff_not_odd]
     tauto
 
+@[simp]
+lemma negOnePow_mul_self (n : ℤ) : (n * n).negOnePow = n.negOnePow := by
+  suffices Even (n * (n - 1)) by
+    simpa [mul_sub, mul_one, negOnePow_eq_iff] using this
+  rw [even_mul]
+  by_cases h : Even (n - 1)
+  · exact Or.inr h
+  · exact Or.inl (by simpa using Int.even_add_one.2 h)
+
 end Int