chore: forward-port leanprover-community/mathlib#18970 (#5852)

This also `#align`s some nearby instance names

Mathlib/Data/Fin/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Keeley Hoek
 
 ! This file was ported from Lean 3 source module data.fin.basic
-! leanprover-community/mathlib commit 008af8bb14b3ebef7e04ec3b0d63b947dee4d26a
+! leanprover-community/mathlib commit 3a2b5524a138b5d0b818b858b516d4ac8a484b03
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -659,6 +659,12 @@ theorem subsingleton_iff_le_one : Subsingleton (Fin n) ↔ n ≤ 1 := by
 
 section Monoid
 
+instance addCommSemigroup (n : ℕ) : AddCommSemigroup (Fin n) where
+  add := (· + ·)
+  add_assoc := by simp [eq_iff_veq, add_def, add_assoc]
+  add_comm := by simp [eq_iff_veq, add_def, add_comm]
+#align fin.add_comm_semigroup Fin.addCommSemigroup
+
 --Porting note: removing `simp`, `simp` can prove it with AddCommMonoid instance
 protected theorem add_zero [NeZero n] (k : Fin n) : k + 0 = k := by
   simp [eq_iff_veq, add_def, mod_eq_of_lt (is_lt k)]
@@ -683,21 +689,20 @@ instance (n) : AddCommSemigroup (Fin n) where
   add_assoc := by simp [eq_iff_veq, add_def, add_assoc]
   add_comm := by simp [eq_iff_veq, add_def, add_comm]
 
-instance addCommMonoid (n : ℕ) [NeZero n] : AddCommMonoid (Fin n)
-    where
+instance addCommMonoid (n : ℕ) [NeZero n] : AddCommMonoid (Fin n) where
   add := (· + ·)
-  add_assoc := by simp [eq_iff_veq, add_def, add_assoc]
   zero := 0
   zero_add := Fin.zero_add
   add_zero := Fin.add_zero
-  add_comm := by simp [eq_iff_veq, add_def, add_comm]
+  __ := Fin.addCommSemigroup n
 #align fin.add_comm_monoid Fin.addCommMonoid
 
-instance (n) [NeZero n] : AddMonoidWithOne (Fin n) where
+instance instAddMonoidWithOne (n) [NeZero n] : AddMonoidWithOne (Fin n) where
   __ := inferInstanceAs (AddCommMonoid (Fin n))
   natCast n := Fin.ofNat'' n
   natCast_zero := rfl
   natCast_succ _ := eq_of_veq (add_mod _ _ _)
+#align fin.add_monoid_with_one Fin.instAddMonoidWithOne
 
 end Monoid
 
@@ -1932,6 +1937,28 @@ instance addCommGroup (n : ℕ) [NeZero n] : AddCommGroup (Fin n) :=
       Fin.ext <| show (a + (n - b)) % n = (a + (n - b) % n) % n by simp
     sub := Fin.sub }
 
+/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
+instance instInvolutiveNeg (n : ℕ) : InvolutiveNeg (Fin n) where
+  neg := Neg.neg
+  neg_neg := Nat.casesOn n finZeroElim fun _i => neg_neg
+#align fin.involutive_neg Fin.instInvolutiveNeg
+
+/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
+instance instIsCancelAdd (n : ℕ) : IsCancelAdd (Fin n) where
+  add_left_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ => add_left_cancel
+  add_right_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ => add_right_cancel
+#align fin.is_cancel_add Fin.instIsCancelAdd
+
+/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
+instance instAddLeftCancelSemigroup (n : ℕ) : AddLeftCancelSemigroup (Fin n) :=
+  { Fin.addCommSemigroup n, Fin.instIsCancelAdd n with }
+#align fin.add_left_cancel_semigroup Fin.instAddLeftCancelSemigroup
+
+/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
+instance instAddRightCancelSemigroup (n : ℕ) : AddRightCancelSemigroup (Fin n) :=
+  { Fin.addCommSemigroup n, Fin.instIsCancelAdd n with }
+#align fin.add_right_cancel_semigroup Fin.instAddRightCancelSemigroup
+
 protected theorem coe_neg (a : Fin n) : ((-a : Fin n) : ℕ) = (n - a) % n :=
   rfl
 #align fin.coe_neg Fin.coe_neg

Mathlib/Data/ZMod/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 
 ! This file was ported from Lean 3 source module data.zmod.defs
-! leanprover-community/mathlib commit 1126441d6bccf98c81214a0780c73d499f6721fe
+! leanprover-community/mathlib commit 3a2b5524a138b5d0b818b858b516d4ac8a484b03
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -46,7 +46,7 @@ to register the ring structure on `ZMod n` as type class instance.
 open Nat.ModEq Int
 
 /-- Multiplicative commutative semigroup structure on `Fin n`. -/
-instance (n : ℕ) : CommSemigroup (Fin n) :=
+instance instCommSemigroup (n : ℕ) : CommSemigroup (Fin n) :=
   { inferInstanceAs (Mul (Fin n)) with
     mul_assoc := fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ =>
       Fin.eq_of_veq <|
@@ -55,6 +55,7 @@ instance (n : ℕ) : CommSemigroup (Fin n) :=
           _ ≡ a * (b * c) [MOD n] := by rw [mul_assoc]
           _ ≡ a * (b * c % n) [MOD n] := (Nat.mod_modEq _ _).symm.mul_left _
     mul_comm := Fin.mul_comm }
+#align fin.comm_semigroup Fin.instCommSemigroup
 
 private theorem left_distrib_aux (n : ℕ) : ∀ a b c : Fin n, a * (b + c) = a * b + a * c :=
   fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ =>
@@ -65,18 +66,30 @@ private theorem left_distrib_aux (n : ℕ) : ∀ a b c : Fin n, a * (b + c) = a
       _ ≡ a * b % n + a * c % n [MOD n] := (Nat.mod_modEq _ _).symm.add (Nat.mod_modEq _ _).symm
 
 /-- Commutative ring structure on `Fin n`. -/
-instance (n : ℕ) [NeZero n] : CommRing (Fin n) :=
-  { Fin.instAddMonoidWithOneFin n, Fin.addCommGroup n,
-    Fin.instCommSemigroupFin n with
-    one_mul := Fin.one_mul
-    mul_one := Fin.mul_one
+instance instDistrib (n : ℕ) : Distrib (Fin n) :=
+  { Fin.addCommSemigroup n, Fin.instCommSemigroup n with
     left_distrib := left_distrib_aux n
     right_distrib := fun a b c => by
-      rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm],
+      rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm] }
+#align fin.distrib Fin.instDistrib
+
+/-- Commutative ring structure on `fin n`. -/
+instance instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n) :=
+  { Fin.instAddMonoidWithOne n, Fin.addCommGroup n, Fin.instCommSemigroup n, Fin.instDistrib n with
+    one_mul := Fin.one_mul
+    mul_one := Fin.mul_one,
     -- porting note: new, see
     -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ring.20vs.20Ring/near/322876462
     zero_mul := Fin.zero_mul
     mul_zero := Fin.mul_zero }
+#align fin.comm_ring Fin.instCommRing
+
+/-- Note this is more general than `fin.comm_ring` as it applies (vacuously) to `fin 0` too. -/
+instance instHasDistribNeg (n : ℕ) : HasDistribNeg (Fin n) :=
+  { toInvolutiveNeg := Fin.instInvolutiveNeg n
+    mul_neg := Nat.casesOn n finZeroElim fun _i => mul_neg
+    neg_mul := Nat.casesOn n finZeroElim fun _i => neg_mul }
+#align fin.has_distrib_neg Fin.instHasDistribNeg
 
 end Fin