[Merged by Bors] - style(RingTheory): fix whitespace

Mathlib/RingTheory/AdicCompletion/LocalRing.lean

@@ -42,7 +42,7 @@ lemma isUnit_iff_notMem_of_isAdicComplete_maximal [IsAdicComplete m R] (r : R) :
       (IsUnit.exists_left_inv (mapu n.2))
     let invSeries : ℕ → R := fun n ↦ if h : n = 0 then 0 else Classical.choose <|
       Ideal.Quotient.mk_surjective <| invSeries' ⟨n, (Nat.zero_lt_of_ne_zero h)⟩
-    have invSeries_spec {n : ℕ} (npos : 0 < n): (Ideal.Quotient.mk (m ^ n)) (invSeries n) =
+    have invSeries_spec {n : ℕ} (npos : 0 < n) : (Ideal.Quotient.mk (m ^ n)) (invSeries n) =
       invSeries' ⟨n, npos⟩ := by
       simpa only [Nat.ne_zero_of_lt npos, invSeries]
       using Classical.choose_spec (Ideal.Quotient.mk_surjective (invSeries' ⟨n, npos⟩))

Mathlib/RingTheory/Binomial.lean

@@ -146,7 +146,7 @@ theorem multichoose_succ_succ (r : R) (k : ℕ) :
     multichoose (r + 1) (k + 1) = multichoose r (k + 1) + multichoose (r + 1) k := by
   rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]
   simp only [factorial_nsmul_multichoose_eq_ascPochhammer, smul_add]
-  rw [add_comm (smeval (ascPochhammer ℕ (k+1)) r), ascPochhammer_succ_succ r k]
+  rw [add_comm (smeval (ascPochhammer ℕ (k + 1)) r), ascPochhammer_succ_succ r k]
 
 @[simp]
 theorem multichoose_one (k : ℕ) : multichoose (1 : R) k = 1 := by
@@ -219,7 +219,7 @@ theorem ascPochhammer_smeval_neg_eq_descPochhammer (r : R) (k : ℕ) :
   | zero => simp
   | succ k ih =>
     simp only [ascPochhammer_succ_right, smeval_mul, ih, descPochhammer_succ_right, sub_eq_add_neg]
-    have h : (X + (k : ℕ[X])).smeval (-r) = - (X + (-k : ℤ[X])).smeval r := by
+    have h : (X + (k : ℕ[X])).smeval (-r) = -(X + (-k : ℤ[X])).smeval r := by
       simp [smeval_natCast, add_comm]
     rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
       Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
@@ -284,7 +284,7 @@ variable {R : Type*} [NonAssocRing R] [Pow R ℕ] [BinomialRing R]
 
 @[simp]
 theorem smeval_ascPochhammer_self_neg : ∀ n : ℕ,
-    smeval (ascPochhammer ℕ n) (-n : ℤ) = (-1)^n * n.factorial
+    smeval (ascPochhammer ℕ n) (-n : ℤ) = (-1) ^ n * n.factorial
   | 0 => by
     rw [Nat.cast_zero, neg_zero, ascPochhammer_zero, Nat.factorial_zero, smeval_one, pow_zero,
       one_smul, pow_zero, Nat.cast_one, one_mul]
@@ -318,7 +318,7 @@ theorem smeval_ascPochhammer_nat_cast {R} [NonAssocSemiring R] [Pow R ℕ] [NatP
     smeval (ascPochhammer ℕ k) (n : R) = smeval (ascPochhammer ℕ k) n := by
   rw [smeval_at_natCast (ascPochhammer ℕ k) n]
 
-theorem multichoose_neg_self (n : ℕ) : multichoose (-n : ℤ) n = (-1)^n := by
+theorem multichoose_neg_self (n : ℕ) : multichoose (-n : ℤ) n = (-1) ^ n := by
   rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
     factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_self_neg, nsmul_eq_mul,
     Nat.cast_comm]

Mathlib/RingTheory/DedekindDomain/Factorization.lean

@@ -427,7 +427,7 @@ theorem count_pow_self (n : ℕ) :
 
 /-- `val_v(I⁻ⁿ) = -val_v(Iⁿ)` for every `n ∈ ℤ`. -/
 theorem count_neg_zpow (n : ℤ) (I : FractionalIdeal R⁰ K) :
-    count K v (I ^ (-n)) = - count K v (I ^ n) := by
+    count K v (I ^ (-n)) = -count K v (I ^ n) := by
   by_cases hI : I = 0
   · by_cases hn : n = 0
     · rw [hn, neg_zero, zpow_zero, count_one, neg_zero]
@@ -437,7 +437,7 @@ theorem count_neg_zpow (n : ℤ) (I : FractionalIdeal R⁰ K) :
     exact count_one K v
 
 theorem count_inv (I : FractionalIdeal R⁰ K) :
-    count K v (I⁻¹) = - count K v I := by
+    count K v (I⁻¹) = -count K v I := by
   rw [← zpow_neg_one, count_neg_zpow K v (1 : ℤ) I, zpow_one]
 
 /-- `val_v(Iⁿ) = n*val_v(I)` for every `n ∈ ℤ`. -/

Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean

@@ -128,7 +128,7 @@ theorem valuation_of_unit_eq (x : Rˣ) :
     exact v.intValuation_le_one _
 
 /-- The multiplicative `v`-adic valuation on `Kˣ` modulo `n`-th powers. -/
-def valuationOfNeZeroMod (n : ℕ) : (K/n) →* Multiplicative (ZMod n) :=
+def valuationOfNeZeroMod (n : ℕ) : (K / n) →* Multiplicative (ZMod n) :=
   -- TODO: this definition does a lot of defeq abuse between `Multiplicative` and `Additive`,
   -- so we need `erw` below.
   (Int.quotientZMultiplesNatEquivZMod n).toMultiplicative.toMonoidHom.comp <|
@@ -142,7 +142,7 @@ def valuationOfNeZeroMod (n : ℕ) : (K/n) →* Multiplicative (ZMod n) :=
 
 @[simp]
 theorem valuation_of_unit_mod_eq (n : ℕ) (x : Rˣ) :
-    v.valuationOfNeZeroMod n (Units.map (algebraMap R K : R →* K) x : K/n) = 1 := by
+    v.valuationOfNeZeroMod n (Units.map (algebraMap R K : R →* K) x : K / n) = 1 := by
   -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
   erw [valuationOfNeZeroMod, MonoidHom.comp_apply, ← QuotientGroup.coe_mk',
     QuotientGroup.map_mk' (G := Kˣ) (N := MonoidHom.range (powMonoidHom n)),
@@ -156,7 +156,7 @@ end HeightOneSpectrum
 variable {S S' : Set <| HeightOneSpectrum R} {n : ℕ}
 
 /-- The Selmer group `K⟮S, n⟯`. -/
-def selmerGroup : Subgroup <| K/n where
+def selmerGroup : Subgroup <| K / n where
   carrier := {x : K/n | ∀ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuationOfNeZeroMod n x = 1}
   one_mem' _ _ := by rw [map_one]
   mul_mem' hx hy v hv := by rw [map_mul, hx v hv, hy v hv, one_mul]
@@ -222,7 +222,7 @@ theorem fromUnit_ker [hn : Fact <| 0 < n] :
       by simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]⟩
 
 /-- The injection induced by the natural homomorphism from `Rˣ` to `K⟮∅, n⟯`. -/
-def fromUnitLift [Fact <| 0 < n] : (R/n) →* K⟮(∅ : Set <| HeightOneSpectrum R),n⟯ :=
+def fromUnitLift [Fact <| 0 < n] : (R / n) →* K⟮(∅ : Set <| HeightOneSpectrum R),n⟯ :=
   (QuotientGroup.kerLift _).comp
     (QuotientGroup.quotientMulEquivOfEq (fromUnit_ker (R := R))).symm.toMonoidHom
 

Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean

@@ -78,7 +78,7 @@ namespace DividedPowers
 structure IsSubDPIdeal {A : Type*} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I)
     (J : Ideal A) : Prop where
   isSubideal : J ≤ I
-  dpow_mem : ∀ (n : ℕ) (_: n ≠ 0) {j : A} (_ : j ∈ J), hI.dpow n j ∈ J
+  dpow_mem : ∀ (n : ℕ) (_ : n ≠ 0) {j : A} (_ : j ∈ J), hI.dpow n j ∈ J
 
 section IsSubDPIdeal
 
@@ -134,7 +134,7 @@ theorem isSubDPIdeal_inf_iff {A : Type*} [CommRing A] {I : Ideal A} (hI : Divide
   · have hab' : a - b ∈ I := I.sub_mem ha hb
     rw [← add_sub_cancel b a, hI.dpow_add' hb hab', range_add_one, sum_insert notMem_range_self,
       tsub_self, hI.dpow_zero hab', mul_one, add_sub_cancel_left]
-    exact J.sum_mem (fun i hi ↦  SemilatticeInf.inf_le_left J I ((J ⊓ I).smul_mem _
+    exact J.sum_mem (fun i hi ↦ SemilatticeInf.inf_le_left J I ((J ⊓ I).smul_mem _
       (hIJ.dpow_mem _ (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩)))
   · refine ⟨SemilatticeInf.inf_le_right J I, fun {n} hn {a} ha ↦ ⟨?_, hI.dpow_mem hn ha.right⟩⟩
     rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]
@@ -161,7 +161,7 @@ theorem span_isSubDPIdeal_iff {S : Set A} (hS : S ⊆ I) :
         apply Submodule.sum_mem (span S)
         intro m _
         by_cases hm0 : m = 0
-        · exact hm0 ▸ mul_mem_left (span S)  _ (hy _ hm)
+        · exact hm0 ▸ mul_mem_left (span S) _ (hy _ hm)
         · exact mul_mem_right _ (span S) (hx _ hm0)
     | smul a x hxI hx =>
         rw [Algebra.id.smul_eq_mul, hI.dpow_mul (hSI hxI)]

Mathlib/RingTheory/Flat/Domain.lean

@@ -70,4 +70,4 @@ This is true over non-domains if one of the modules is flat.
 See `LinearIndepOn.tmul_of_flat_left`. -/
 nonrec lemma LinearIndepOn.tmul_of_isDomain (hv : LinearIndepOn R v s) (hw : LinearIndepOn R w t) :
     LinearIndepOn R (fun i : ι × κ ↦ v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t) :=
-  ((hv.tmul_of_isDomain hw).comp _ (Equiv.Set.prod _ _).injective:)
+  ((hv.tmul_of_isDomain hw).comp _ (Equiv.Set.prod _ _).injective :)

Mathlib/RingTheory/Grassmannian.lean

@@ -67,7 +67,7 @@ attribute [instance] Grassmannian.finite_quotient Grassmannian.projective_quotie
 
 namespace Grassmannian
 
-@[inherit_doc] scoped notation "G("k", "M"; "R")" => Grassmannian R M k
+@[inherit_doc] scoped notation "G(" k ", " M "; " R ")" => Grassmannian R M k
 
 variable {R M k}
 

Mathlib/RingTheory/HahnSeries/HEval.lean

@@ -72,7 +72,7 @@ theorem powerSeriesFamily_hsum_zero (f : PowerSeries R) :
 theorem powerSeriesFamily_add {x : HahnSeries Γ V} (f g : PowerSeries R) :
     powerSeriesFamily x (f + g) = powerSeriesFamily x f + powerSeriesFamily x g := by
   ext1 n
-  by_cases hx: 0 < x.orderTop <;> · simp [hx, add_smul]
+  by_cases hx : 0 < x.orderTop <;> · simp [hx, add_smul]
 
 theorem powerSeriesFamily_smul {x : HahnSeries Γ V} (f : PowerSeries R) (r : R) :
     powerSeriesFamily x (r • f) = HahnSeries.single (0 : Γ) r • powerSeriesFamily x f := by

Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

@@ -44,7 +44,7 @@ def quotEquivPowQuotPowSucc (h : I.IsPrincipal) (h' : I ≠ ⊥) (n : ℕ) :
   let ϖ := h.principal.choose
   have hI : I = Ideal.span {ϖ} := h.principal.choose_spec
   have hϖ : ϖ ^ n ∈ I ^ n := hI ▸ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) n)
-  let g : R →ₗ[R] (I ^ n : Ideal R) := (LinearMap.mulRight R ϖ^n).codRestrict _ fun x ↦ by
+  let g : R →ₗ[R] (I ^ n : Ideal R) := (LinearMap.mulRight R ϖ ^ n).codRestrict _ fun x ↦ by
     simp only [LinearMap.pow_mulRight, LinearMap.mulRight_apply]
     -- TODO: change argument of Ideal.pow_mem_of_mem
     exact Ideal.mul_mem_left _ _ hϖ

Mathlib/RingTheory/Invariant/Basic.lean

@@ -101,7 +101,7 @@ instance (H : Subgroup G) [H.Normal] :
   inferInstanceAs (MulSemiringAction (G ⧸ H) (FixedPoints.subring B H))
 
 instance (H : Subgroup G) [H.Normal] :
-    SMulCommClass (G ⧸ H) A (FixedPoints.subalgebra A B H)  where
+    SMulCommClass (G ⧸ H) A (FixedPoints.subalgebra A B H) where
   smul_comm := Quotient.ind fun g r h ↦ Subtype.ext (smul_comm g r h.1)
 
 instance (H : Subgroup G) [H.Normal] [Algebra.IsInvariant A B G] :
@@ -256,7 +256,7 @@ private theorem fixed_of_fixed1_aux1 [DecidableEq (Ideal B)] :
     have hr : r = ∑ i ∈ Finset.range (k + 1), Polynomial.monomial i (f.coeff (i + j)) := rfl
     rw [← Ideal.neg_mem_iff, neg_sub, hr, Finset.sum_range_succ', Polynomial.eval_add,
         Polynomial.eval_monomial, zero_add, pow_zero, mul_one, add_sub_cancel_right]
-    simp only [ ← Polynomial.monomial_mul_X]
+    simp only [← Polynomial.monomial_mul_X]
     rw [← Finset.sum_mul, Polynomial.eval_mul_X]
     exact Ideal.mul_mem_left (g • Q) _ (hbP g hg)
   refine ⟨a, a - r.eval b, ha, ?_, fun h ↦ ?_⟩

Mathlib/RingTheory/LaurentSeries.lean

@@ -441,8 +441,8 @@ theorem intValuation_eq_of_coe (P : K[X]) :
     simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, coe_eq_zero_iff, hP,
       not_false_eq_true, true_and, (idealX K).3]
   classical
-  rw [count_associates_factors_eq  (span_ne_zero).1
-    (Ideal.span_singleton_prime Polynomial.X_ne_zero|>.mpr prime_X) (span_ne_zero).2,
+  rw [count_associates_factors_eq (span_ne_zero).1
+    (Ideal.span_singleton_prime Polynomial.X_ne_zero |>.mpr prime_X) (span_ne_zero).2,
     count_associates_factors_eq]
   on_goal 1 => convert (normalized_count_X_eq_of_coe hP).symm
   exacts [count_span_normalizedFactors_eq_of_normUnit hP Polynomial.normUnit_X prime_X,
@@ -808,7 +808,7 @@ theorem exists_Polynomial_intValuation_lt (F : K⟦X⟧) (η : ℤᵐ⁰ˣ) :
       apply (intValuation_le_iff_coeff_lt_eq_zero K _).mpr
       simpa only [map_sub, sub_eq_zero, Polynomial.coeff_coe, coeff_trunc] using
         fun _ h ↦ (if_pos h).symm
-    rw [ neg_add, ofAdd_add, ← hd, ofAdd_toAdd, WithZero.coe_mul, coe_unzero,
+    rw [neg_add, ofAdd_add, ← hd, ofAdd_toAdd, WithZero.coe_mul, coe_unzero,
       ← coe_algebraMap] at this
     rw [← valuation_of_algebraMap (K := K⸨X⸩) (PowerSeries.idealX K) (F - F.trunc (d + 1))]
     apply lt_of_le_of_lt this

Mathlib/RingTheory/Localization/Defs.lean

@@ -903,7 +903,7 @@ namespace IsLocalization
 variable [IsLocalization M S]
 
 theorem mk'_neg (x : R) (y : M) :
-    mk' S (-x) y = - mk' S x y := by
+    mk' S (-x) y = -mk' S x y := by
   rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]
 
 theorem mk'_sub (x₁ x₂ : R) (y₁ y₂ : M) :

Mathlib/RingTheory/MvPowerSeries/Evaluation.lean

@@ -341,7 +341,7 @@ theorem comp_aeval (ha : HasEval a)
     [IsTopologicalRing T] [IsLinearTopology T T]
     [T2Space T] [Algebra R T] [ContinuousSMul R T] [CompleteSpace T]
     {ε : S →ₐ[R] T} (hε : Continuous ε) :
-    ε.comp (aeval ha) = aeval (ha.map hε)  := by
+    ε.comp (aeval ha) = aeval (ha.map hε) := by
   apply DFunLike.ext'
   simp only [AlgHom.coe_comp, coe_aeval ha]
   rw [← RingHom.coe_coe,

Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean

@@ -129,13 +129,13 @@ lemma hasBasis_nhds_zero [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R]
   when the ring of coefficients has a linear topology. -/
 instance [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :
     IsLinearTopology (MvPowerSeries σ R) (MvPowerSeries σ R) :=
-  IsLinearTopology.mk_of_hasBasis'  _ hasBasis_nhds_zero TwoSidedIdeal.mul_mem_left
+  IsLinearTopology.mk_of_hasBasis' _ hasBasis_nhds_zero TwoSidedIdeal.mul_mem_left
 
 /-- The topology on `MvPowerSeries` is a right linear topology
   when the ring of coefficients has a linear topology. -/
 instance [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :
     IsLinearTopology (MvPowerSeries σ R)ᵐᵒᵖ (MvPowerSeries σ R) :=
-  IsLinearTopology.mk_of_hasBasis'  _ hasBasis_nhds_zero (fun J _ _ hg ↦ J.mul_mem_right _ _ hg)
+  IsLinearTopology.mk_of_hasBasis' _ hasBasis_nhds_zero (fun J _ _ hg ↦ J.mul_mem_right _ _ hg)
 
 theorem isTopologicallyNilpotent_of_constantCoeff
     {R : Type*} [CommRing R] [TopologicalSpace R] [IsLinearTopology R R]

Mathlib/RingTheory/Nilpotent/Exp.lean

@@ -90,9 +90,9 @@ theorem exp_add_of_commute {a b : A} (h₁ : Commute a b) (h₂ : IsNilpotent a)
     calc ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • (a + b) ^ i
         = ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * i.choose j := ?_
       _ = ∑ i ∈ R2N, (∑ j ∈ range (i + 1),
-            ((j ! : ℚ)⁻¹ * ((i - j) ! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_
+            ((j ! : ℚ)⁻¹ * ((i - j)! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_
       _ = ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
-            ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
+            ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
     · refine sum_congr rfl fun i _ ↦ ?_
       rw [Commute.add_pow h₁ i]
     · simp_rw [smul_sum]
@@ -119,32 +119,32 @@ theorem exp_add_of_commute {a b : A} (h₁ : Commute a b) (h₂ : IsNilpotent a)
         exact fun x y _ _ _ ↦ ⟨x + y, x, by cutsat⟩
       · simp only [mem_sigma, mem_range, implies_true]
   have z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ ij.1 + ij.2 ≤ 2 * N,
-      ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0 :=
+      ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0 :=
     sum_eq_zero fun i hi ↦ by
       rw [mem_filter] at hi
       cases le_or_gt (N + 1) i.1 with
         | inl h => rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
         | inr _ => rw [pow_eq_zero_of_le (by linarith) h₅, mul_zero, smul_zero]
   have split₁ := sum_filter_add_sum_filter_not (R2N ×ˢ R2N)
     (fun ij ↦ ij.1 + ij.2 ≤ 2 * N)
-    (fun ij ↦ ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2))
+    (fun ij ↦ ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2))
   rw [z₁, add_zero] at split₁
   rw [split₁] at s₁
   have z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬ (ij.1 ≤ N ∧ ij.2 ≤ N),
-      ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0 :=
+      ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0 :=
     sum_eq_zero fun i hi ↦ by
     simp only [not_and, not_le, mem_filter] at hi
     cases le_or_gt (N + 1) i.1 with
       | inl h => rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
       | inr h => rw [pow_eq_zero_of_le (hi.2 (Nat.le_of_lt_succ h)) h₅, mul_zero, smul_zero]
   have split₂ := sum_filter_add_sum_filter_not (R2N ×ˢ R2N)
     (fun ij ↦ ij.1 ≤ N ∧ ij.2 ≤ N)
-    (fun ij ↦ ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2))
+    (fun ij ↦ ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2))
   rw [z₂, add_zero] at split₂
   rw [← split₂] at s₁
-  have restrict: ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N,
-      ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
-        ∑ ij ∈ RN ×ˢ RN, ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := by
+  have restrict : ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N,
+      ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
+        ∑ ij ∈ RN ×ˢ RN, ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := by
     apply sum_congr
     · ext x
       simp only [mem_filter, mem_product, mem_range, hR2N, hRN]
@@ -154,7 +154,7 @@ theorem exp_add_of_commute {a b : A} (h₁ : Commute a b) (h₂ : IsNilpotent a)
   have s₂ := by
     calc (∑ i ∈ RN, (i ! : ℚ)⁻¹ • a ^ i) * ∑ i ∈ RN, (i ! : ℚ)⁻¹ • b ^ i
         = ∑ i ∈ RN, ∑ j ∈ RN, ((i ! : ℚ)⁻¹ * (j ! : ℚ)⁻¹) • (a ^ i * b ^ j) := ?_
-      _ = ∑ ij ∈ RN ×ˢ RN, ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
+      _ = ∑ ij ∈ RN ×ˢ RN, ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
     · rw [sum_mul_sum]
       refine sum_congr rfl fun _ _ ↦ sum_congr rfl fun _ _ ↦ ?_
       rw [smul_mul_assoc, mul_smul_comm, smul_smul]
@@ -175,12 +175,12 @@ theorem exp_mul_exp_neg_self {a : A} (h : IsNilpotent a) :
   simp [← exp_add_of_commute (Commute.neg_right rfl) h h.neg]
 
 theorem exp_neg_mul_exp_self {a : A} (h : IsNilpotent a) :
-    exp (- a) * exp a = 1 := by
+    exp (-a) * exp a = 1 := by
   simp [← exp_add_of_commute (Commute.neg_left rfl) h.neg h]
 
 theorem isUnit_exp {a : A} (h : IsNilpotent a) : IsUnit (exp a) := by
   apply isUnit_iff_exists.2
-  use exp (- a)
+  use exp (-a)
   exact ⟨exp_mul_exp_neg_self h, exp_neg_mul_exp_self h⟩
 
 @[deprecated (since := "2025-03-11")]

Mathlib/RingTheory/Norm/Transitivity.lean

@@ -104,7 +104,7 @@ omit [Fintype m] in
 lemma polyToMatrix_cornerAddX :
     f.polyToMatrix (cornerAddX M k k k) = (-f (M k k)).charmatrix := by
   simp [cornerAddX, Matrix.add_apply, charmatrix,
-    RingHom.polyToMatrix, - AlgEquiv.symm_toRingEquiv, map_neg]
+    RingHom.polyToMatrix, -AlgEquiv.symm_toRingEquiv, map_neg]
 
 lemma eval_zero_det_det : eval 0 (f.polyToMatrix (cornerAddX M k).det).det = (f M.det).det := by
   rw [← coe_evalRingHom, RingHom.map_det, ← RingHom.comp_apply,