chore: remove space after ⅟ (#26997)

This will change how the docs and infoview render, and the rules for the upcoming whitespace linter.

Zulip thread: [#mathlib4 > Space after `⅟ ` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Space.20after.20.60.E2.85.9F.20.60/near/528309060)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: eric-wieser

Mathlib/Algebra/Group/Action/Basic.lean

@@ -68,7 +68,7 @@ section Monoid
 variable [Monoid α] [MulAction α β] (c : α) (x y : β) [Invertible c]
 
 @[simp] lemma invOf_smul_smul : ⅟c • c • x = x := inv_smul_smul (unitOfInvertible c) _
-@[simp] lemma smul_invOf_smul : c • (⅟ c • x) = x := smul_inv_smul (unitOfInvertible c) _
+@[simp] lemma smul_invOf_smul : c • (⅟c • x) = x := smul_inv_smul (unitOfInvertible c) _
 
 variable {c x y}
 

Mathlib/Algebra/Group/Invertible/Basic.lean

@@ -22,7 +22,7 @@ variable {α : Type u}
 @[simps]
 def unitOfInvertible [Monoid α] (a : α) [Invertible a] : αˣ where
   val := a
-  inv := ⅟ a
+  inv := ⅟a
   val_inv := by simp
   inv_val := by simp
 
@@ -37,7 +37,7 @@ def Units.invertible [Monoid α] (u : αˣ) :
   mul_invOf_self := u.mul_inv
 
 @[simp]
-theorem invOf_units [Monoid α] (u : αˣ) [Invertible (u : α)] : ⅟ (u : α) = ↑u⁻¹ :=
+theorem invOf_units [Monoid α] (u : αˣ) [Invertible (u : α)] : ⅟(u : α) = ↑u⁻¹ :=
   invOf_eq_right_inv u.mul_inv
 
 theorem IsUnit.nonempty_invertible [Monoid α] {a : α} (h : IsUnit a) : Nonempty (Invertible a) :=
@@ -55,39 +55,39 @@ theorem nonempty_invertible_iff_isUnit [Monoid α] (a : α) : Nonempty (Invertib
   ⟨Nonempty.rec <| @isUnit_of_invertible _ _ _, IsUnit.nonempty_invertible⟩
 
 theorem Commute.invOf_right [Monoid α] {a b : α} [Invertible b] (h : Commute a b) :
-    Commute a (⅟ b) :=
+    Commute a (⅟b) :=
   calc
-    a * ⅟ b = ⅟ b * (b * a * ⅟ b) := by simp [mul_assoc]
-    _ = ⅟ b * (a * b * ⅟ b) := by rw [h.eq]
-    _ = ⅟ b * a := by simp [mul_assoc]
+    a * ⅟b = ⅟b * (b * a * ⅟b) := by simp [mul_assoc]
+    _ = ⅟b * (a * b * ⅟b) := by rw [h.eq]
+    _ = ⅟b * a := by simp [mul_assoc]
 
 theorem Commute.invOf_left [Monoid α] {a b : α} [Invertible b] (h : Commute b a) :
-    Commute (⅟ b) a :=
+    Commute (⅟b) a :=
   calc
-    ⅟ b * a = ⅟ b * (a * b * ⅟ b) := by simp [mul_assoc]
-    _ = ⅟ b * (b * a * ⅟ b) := by rw [h.eq]
-    _ = a * ⅟ b := by simp [mul_assoc]
+    ⅟b * a = ⅟b * (a * b * ⅟b) := by simp [mul_assoc]
+    _ = ⅟b * (b * a * ⅟b) := by rw [h.eq]
+    _ = a * ⅟b := by simp [mul_assoc]
 
-theorem commute_invOf {M : Type*} [One M] [Mul M] (m : M) [Invertible m] : Commute m (⅟ m) :=
+theorem commute_invOf {M : Type*} [One M] [Mul M] (m : M) [Invertible m] : Commute m (⅟m) :=
   calc
-    m * ⅟ m = 1 := mul_invOf_self m
-    _ = ⅟ m * m := (invOf_mul_self m).symm
+    m * ⅟m = 1 := mul_invOf_self m
+    _ = ⅟m * m := (invOf_mul_self m).symm
 
 section Monoid
 
 variable [Monoid α]
 
 /-- This is the `Invertible` version of `Units.isUnit_units_mul` -/
 abbrev invertibleOfInvertibleMul (a b : α) [Invertible a] [Invertible (a * b)] : Invertible b where
-  invOf := ⅟ (a * b) * a
+  invOf := ⅟(a * b) * a
   invOf_mul_self := by rw [mul_assoc, invOf_mul_self]
   mul_invOf_self := by
     rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
       one_mul]
 
 /-- This is the `Invertible` version of `Units.isUnit_mul_units` -/
 abbrev invertibleOfMulInvertible (a b : α) [Invertible (a * b)] [Invertible b] : Invertible a where
-  invOf := b * ⅟ (a * b)
+  invOf := b * ⅟(a * b)
   invOf_mul_self := by
     rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
       one_mul]
@@ -110,11 +110,11 @@ def Invertible.mulRight (a : α) {b : α} (_ : Invertible b) : Invertible a ≃
   right_inv _ := Subsingleton.elim _ _
 
 instance invertiblePow (m : α) [Invertible m] (n : ℕ) : Invertible (m ^ n) where
-  invOf := ⅟ m ^ n
+  invOf := ⅟m ^ n
   invOf_mul_self := by rw [← (commute_invOf m).symm.mul_pow, invOf_mul_self, one_pow]
   mul_invOf_self := by rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]
 
-lemma invOf_pow (m : α) [Invertible m] (n : ℕ) [Invertible (m ^ n)] : ⅟ (m ^ n) = ⅟ m ^ n :=
+lemma invOf_pow (m : α) [Invertible m] (n : ℕ) [Invertible (m ^ n)] : ⅟(m ^ n) = ⅟m ^ n :=
   @invertible_unique _ _ _ _ _ (invertiblePow m n) rfl
 
 /-- If `x ^ n = 1` then `x` has an inverse, `x^(n - 1)`. -/
@@ -128,7 +128,7 @@ end Monoid
 def Invertible.map {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [MulOneClass S]
     [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R) [Invertible r] :
     Invertible (f r) where
-  invOf := f (⅟ r)
+  invOf := f (⅟r)
   invOf_mul_self := by rw [← map_mul, invOf_mul_self, map_one]
   mul_invOf_self := by rw [← map_mul, mul_invOf_self, map_one]
 
@@ -137,7 +137,7 @@ before applying this lemma. -/
 theorem map_invOf {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [Monoid S]
     [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R)
     [Invertible r] [ifr : Invertible (f r)] :
-    f (⅟ r) = ⅟ (f r) :=
+    f (⅟r) = ⅟(f r) :=
   have h : ifr = Invertible.map f r := Subsingleton.elim _ _
   by subst h; rfl
 

Mathlib/Algebra/Group/Invertible/Defs.lean

@@ -90,60 +90,60 @@ class Invertible [Mul α] [One α] (a : α) : Type u where
 
 /-- The inverse of an `Invertible` element -/
 -- This notation has the same precedence as `Inv.inv`.
-prefix:max "⅟ " => Invertible.invOf
+prefix:max "⅟" => Invertible.invOf
 
 @[simp]
-theorem invOf_mul_self' [Mul α] [One α] (a : α) {_ : Invertible a} : ⅟ a * a = 1 :=
+theorem invOf_mul_self' [Mul α] [One α] (a : α) {_ : Invertible a} : ⅟a * a = 1 :=
   Invertible.invOf_mul_self
 
-theorem invOf_mul_self [Mul α] [One α] (a : α) [Invertible a] : ⅟ a * a = 1 := invOf_mul_self' _
+theorem invOf_mul_self [Mul α] [One α] (a : α) [Invertible a] : ⅟a * a = 1 := invOf_mul_self' _
 
 @[simp]
-theorem mul_invOf_self' [Mul α] [One α] (a : α) {_ : Invertible a} : a * ⅟ a = 1 :=
+theorem mul_invOf_self' [Mul α] [One α] (a : α) {_ : Invertible a} : a * ⅟a = 1 :=
   Invertible.mul_invOf_self
 
-theorem mul_invOf_self [Mul α] [One α] (a : α) [Invertible a] : a * ⅟ a = 1 := mul_invOf_self' _
+theorem mul_invOf_self [Mul α] [One α] (a : α) [Invertible a] : a * ⅟a = 1 := mul_invOf_self' _
 
 @[simp]
-theorem invOf_mul_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : ⅟ a * (a * b) = b := by
+theorem invOf_mul_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : ⅟a * (a * b) = b := by
   rw [← mul_assoc, invOf_mul_self, one_mul]
 example {G} [Group G] (a b : G) : a⁻¹ * (a * b) = b := inv_mul_cancel_left a b
 
-theorem invOf_mul_cancel_left [Monoid α] (a b : α) [Invertible a] : ⅟ a * (a * b) = b :=
+theorem invOf_mul_cancel_left [Monoid α] (a b : α) [Invertible a] : ⅟a * (a * b) = b :=
   invOf_mul_cancel_left' _ _
 
 @[simp]
-theorem mul_invOf_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : a * (⅟ a * b) = b := by
+theorem mul_invOf_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : a * (⅟a * b) = b := by
   rw [← mul_assoc, mul_invOf_self, one_mul]
 example {G} [Group G] (a b : G) : a * (a⁻¹ * b) = b := mul_inv_cancel_left a b
 
-theorem mul_invOf_cancel_left [Monoid α] (a b : α) [Invertible a] : a * (⅟ a * b) = b :=
+theorem mul_invOf_cancel_left [Monoid α] (a b : α) [Invertible a] : a * (⅟a * b) = b :=
   mul_invOf_cancel_left' a b
 
 @[simp]
-theorem invOf_mul_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * ⅟ b * b = a := by
+theorem invOf_mul_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * ⅟b * b = a := by
   simp [mul_assoc]
 example {G} [Group G] (a b : G) : a * b⁻¹ * b = a := inv_mul_cancel_right a b
 
-theorem invOf_mul_cancel_right [Monoid α] (a b : α) [Invertible b] : a * ⅟ b * b = a :=
+theorem invOf_mul_cancel_right [Monoid α] (a b : α) [Invertible b] : a * ⅟b * b = a :=
   invOf_mul_cancel_right' _ _
 
 @[simp]
-theorem mul_invOf_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * b * ⅟ b = a := by
+theorem mul_invOf_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * b * ⅟b = a := by
   simp [mul_assoc]
 example {G} [Group G] (a b : G) : a * b * b⁻¹ = a := mul_inv_cancel_right a b
 
-theorem mul_invOf_cancel_right [Monoid α] (a b : α) [Invertible b] : a * b * ⅟ b = a :=
+theorem mul_invOf_cancel_right [Monoid α] (a b : α) [Invertible b] : a * b * ⅟b = a :=
   mul_invOf_cancel_right' _ _
 
-theorem invOf_eq_right_inv [Monoid α] {a b : α} [Invertible a] (hac : a * b = 1) : ⅟ a = b :=
+theorem invOf_eq_right_inv [Monoid α] {a b : α} [Invertible a] (hac : a * b = 1) : ⅟a = b :=
   left_inv_eq_right_inv (invOf_mul_self _) hac
 
-theorem invOf_eq_left_inv [Monoid α] {a b : α} [Invertible a] (hac : b * a = 1) : ⅟ a = b :=
+theorem invOf_eq_left_inv [Monoid α] {a b : α} [Invertible a] (hac : b * a = 1) : ⅟a = b :=
   (left_inv_eq_right_inv hac (mul_invOf_self _)).symm
 
 theorem invertible_unique {α : Type u} [Monoid α] (a b : α) [Invertible a] [Invertible b]
-    (h : a = b) : ⅟ a = ⅟ b := by
+    (h : a = b) : ⅟a = ⅟b := by
   apply invOf_eq_right_inv
   rw [h, mul_invOf_self]
 
@@ -159,7 +159,7 @@ theorem Invertible.congr [Monoid α] (a b : α) [Invertible a] [Invertible b] (h
 
 /-- If `r` is invertible and `s = r` and `si = ⅟r`, then `s` is invertible with `⅟s = si`. -/
 def Invertible.copy' [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (si : α) (hs : s = r)
-    (hsi : si = ⅟ r) : Invertible s where
+    (hsi : si = ⅟r) : Invertible s where
   invOf := si
   invOf_mul_self := by rw [hs, hsi, invOf_mul_self]
   mul_invOf_self := by rw [hs, hsi, mul_invOf_self]
@@ -174,38 +174,38 @@ def invertibleOfGroup [Group α] (a : α) : Invertible a :=
   ⟨a⁻¹, inv_mul_cancel a, mul_inv_cancel a⟩
 
 @[simp]
-theorem invOf_eq_group_inv [Group α] (a : α) [Invertible a] : ⅟ a = a⁻¹ :=
+theorem invOf_eq_group_inv [Group α] (a : α) [Invertible a] : ⅟a = a⁻¹ :=
   invOf_eq_right_inv (mul_inv_cancel a)
 
 /-- `1` is the inverse of itself -/
 def invertibleOne [Monoid α] : Invertible (1 : α) :=
   ⟨1, mul_one _, one_mul _⟩
 
 @[simp]
-theorem invOf_one' [Monoid α] {_ : Invertible (1 : α)} : ⅟ (1 : α) = 1 :=
+theorem invOf_one' [Monoid α] {_ : Invertible (1 : α)} : ⅟(1 : α) = 1 :=
   invOf_eq_right_inv (mul_one _)
 
-theorem invOf_one [Monoid α] [Invertible (1 : α)] : ⅟ (1 : α) = 1 := invOf_one'
+theorem invOf_one [Monoid α] [Invertible (1 : α)] : ⅟(1 : α) = 1 := invOf_one'
 
 /-- `a` is the inverse of `⅟a`. -/
-instance invertibleInvOf [One α] [Mul α] {a : α} [Invertible a] : Invertible (⅟ a) :=
+instance invertibleInvOf [One α] [Mul α] {a : α} [Invertible a] : Invertible (⅟a) :=
   ⟨a, mul_invOf_self a, invOf_mul_self a⟩
 
 @[simp]
-theorem invOf_invOf [Monoid α] (a : α) [Invertible a] [Invertible (⅟ a)] : ⅟ (⅟ a) = a :=
+theorem invOf_invOf [Monoid α] (a : α) [Invertible a] [Invertible (⅟a)] : ⅟(⅟a) = a :=
   invOf_eq_right_inv (invOf_mul_self _)
 
 @[simp]
-theorem invOf_inj [Monoid α] {a b : α} [Invertible a] [Invertible b] : ⅟ a = ⅟ b ↔ a = b :=
+theorem invOf_inj [Monoid α] {a b : α} [Invertible a] [Invertible b] : ⅟a = ⅟b ↔ a = b :=
   ⟨invertible_unique _ _, invertible_unique _ _⟩
 
 /-- `⅟b * ⅟a` is the inverse of `a * b` -/
 def invertibleMul [Monoid α] (a b : α) [Invertible a] [Invertible b] : Invertible (a * b) :=
-  ⟨⅟ b * ⅟ a, by simp [← mul_assoc], by simp [← mul_assoc]⟩
+  ⟨⅟b * ⅟a, by simp [← mul_assoc], by simp [← mul_assoc]⟩
 
 @[simp]
 theorem invOf_mul [Monoid α] (a b : α) [Invertible a] [Invertible b] [Invertible (a * b)] :
-    ⅟ (a * b) = ⅟ b * ⅟ a :=
+    ⅟(a * b) = ⅟b * ⅟a :=
   invOf_eq_right_inv (by simp [← mul_assoc])
 
 /-- A copy of `invertibleMul` for dot notation. -/

Mathlib/Algebra/GroupWithZero/Invertible.lean

@@ -22,7 +22,7 @@ theorem Invertible.ne_zero [MulZeroOneClass α] (a : α) [Nontrivial α] [Invert
   fun ha =>
   zero_ne_one <|
     calc
-      0 = ⅟ a * a := by simp [ha]
+      0 = ⅟a * a := by simp [ha]
       _ = 1 := invOf_mul_self
 
 instance (priority := 100) Invertible.toNeZero [MulZeroOneClass α] [Nontrivial α] (a : α)
@@ -34,7 +34,7 @@ variable [MonoidWithZero α]
 
 /-- A variant of `Ring.inverse_unit`. -/
 @[simp]
-theorem Ring.inverse_invertible (x : α) [Invertible x] : Ring.inverse x = ⅟ x :=
+theorem Ring.inverse_invertible (x : α) [Invertible x] : Ring.inverse x = ⅟x :=
   Ring.inverse_unit (unitOfInvertible _)
 
 end MonoidWithZero
@@ -47,7 +47,7 @@ def invertibleOfNonzero {a : α} (h : a ≠ 0) : Invertible a :=
   ⟨a⁻¹, inv_mul_cancel₀ h, mul_inv_cancel₀ h⟩
 
 @[simp]
-theorem invOf_eq_inv (a : α) [Invertible a] : ⅟ a = a⁻¹ :=
+theorem invOf_eq_inv (a : α) [Invertible a] : ⅟a = a⁻¹ :=
   invOf_eq_right_inv (mul_inv_cancel₀ (Invertible.ne_zero a))
 
 @[simp]
@@ -79,7 +79,7 @@ def invertibleDiv (a b : α) [Invertible a] [Invertible b] : Invertible (a / b)
   ⟨b / a, by simp [← mul_div_assoc], by simp [← mul_div_assoc]⟩
 
 theorem invOf_div (a b : α) [Invertible a] [Invertible b] [Invertible (a / b)] :
-    ⅟ (a / b) = b / a :=
+    ⅟(a / b) = b / a :=
   invOf_eq_right_inv (by simp [← mul_div_assoc])
 
 end GroupWithZero

Mathlib/Algebra/Lie/Classical.lean

@@ -276,7 +276,7 @@ theorem jd_transform [Fintype l] : (PD l R)ᵀ * JD l R * PD l R = (2 : R) • S
   rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]
   simp [two_smul]
 
-theorem pd_inv [Fintype l] [Invertible (2 : R)] : PD l R * ⅟ (2 : R) • (PD l R)ᵀ = 1 := by
+theorem pd_inv [Fintype l] [Invertible (2 : R)] : PD l R * ⅟(2 : R) • (PD l R)ᵀ = 1 := by
   rw [PD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul,
     Matrix.fromBlocks_multiply]
   simp
@@ -335,7 +335,7 @@ def PB :=
 
 variable [Fintype l]
 
-theorem pb_inv [Invertible (2 : R)] : PB l R * Matrix.fromBlocks 1 0 0 (⅟ (PD l R)) = 1 := by
+theorem pb_inv [Invertible (2 : R)] : PB l R * Matrix.fromBlocks 1 0 0 (⅟(PD l R)) = 1 := by
   rw [PB, Matrix.fromBlocks_multiply, mul_invOf_self]
   simp only [Matrix.mul_zero, Matrix.mul_one, Matrix.zero_mul, zero_add, add_zero,
     Matrix.fromBlocks_one]

Mathlib/Algebra/Module/Basic.lean

@@ -32,7 +32,7 @@ theorem Units.neg_smul [Ring R] [AddCommGroup M] [Module R M] (u : Rˣ) (x : M)
 @[simp]
 theorem invOf_two_smul_add_invOf_two_smul (R) [Semiring R] [AddCommMonoid M] [Module R M]
     [Invertible (2 : R)] (x : M) :
-    (⅟ 2 : R) • x + (⅟ 2 : R) • x = x :=
+    (⅟2 : R) • x + (⅟2 : R) • x = x :=
   Convex.combo_self invOf_two_add_invOf_two _
 
 theorem map_inv_natCast_smul [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂]

Mathlib/Algebra/Order/Invertible.lean

@@ -14,23 +14,23 @@ import Mathlib.Data.Nat.Cast.Order.Ring
 variable {R : Type*} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R}
 
 @[simp]
-theorem invOf_pos [Invertible a] : 0 < ⅟ a ↔ 0 < a :=
-  haveI : 0 < a * ⅟ a := by simp only [mul_invOf_self, zero_lt_one]
+theorem invOf_pos [Invertible a] : 0 < ⅟a ↔ 0 < a :=
+  haveI : 0 < a * ⅟a := by simp only [mul_invOf_self, zero_lt_one]
   ⟨fun h => pos_of_mul_pos_left this h.le, fun h => pos_of_mul_pos_right this h.le⟩
 
 @[simp]
-theorem invOf_nonpos [Invertible a] : ⅟ a ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, invOf_pos]
+theorem invOf_nonpos [Invertible a] : ⅟a ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, invOf_pos]
 
 @[simp]
-theorem invOf_nonneg [Invertible a] : 0 ≤ ⅟ a ↔ 0 ≤ a :=
-  haveI : 0 < a * ⅟ a := by simp only [mul_invOf_self, zero_lt_one]
+theorem invOf_nonneg [Invertible a] : 0 ≤ ⅟a ↔ 0 ≤ a :=
+  haveI : 0 < a * ⅟a := by simp only [mul_invOf_self, zero_lt_one]
   ⟨fun h => (pos_of_mul_pos_left this h).le, fun h => (pos_of_mul_pos_right this h).le⟩
 
 @[simp]
-theorem invOf_lt_zero [Invertible a] : ⅟ a < 0 ↔ a < 0 := by simp only [← not_le, invOf_nonneg]
+theorem invOf_lt_zero [Invertible a] : ⅟a < 0 ↔ a < 0 := by simp only [← not_le, invOf_nonneg]
 
 @[simp]
-theorem invOf_le_one [Invertible a] (h : 1 ≤ a) : ⅟ a ≤ 1 :=
+theorem invOf_le_one [Invertible a] (h : 1 ≤ a) : ⅟a ≤ 1 :=
   mul_invOf_self a ▸ le_mul_of_one_le_left (invOf_nonneg.2 <| zero_le_one.trans h) h
 
 theorem pos_invOf_of_invertible_cast [Nontrivial R] (n : ℕ)

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -293,11 +293,11 @@ theorem algEquivOfCompEqX_symm (p q : R[X]) (hpq : p.comp q = X) (hqp : q.comp p
   with inverse `p(X) ↦ p(a⁻¹ * (X - b))`. -/
 @[simps!]
 def algEquivCMulXAddC {R : Type*} [CommRing R] (a b : R) [Invertible a] : R[X] ≃ₐ[R] R[X] :=
-  algEquivOfCompEqX (C a * X + C b) (C ⅟ a * (X - C b))
+  algEquivOfCompEqX (C a * X + C b) (C ⅟a * (X - C b))
     (by simp [← C_mul, ← mul_assoc]) (by simp [← C_mul, ← mul_assoc])
 
 theorem algEquivCMulXAddC_symm_eq {R : Type*} [CommRing R] (a b : R) [Invertible a] :
-    (algEquivCMulXAddC a b).symm =  algEquivCMulXAddC (⅟ a) (- ⅟ a * b) := by
+    (algEquivCMulXAddC a b).symm =  algEquivCMulXAddC (⅟a) (- ⅟a * b) := by
   ext p : 1
   simp only [algEquivCMulXAddC_symm_apply, neg_mul, algEquivCMulXAddC_apply, map_neg, map_mul]
   congr
@@ -585,7 +585,7 @@ lemma comp_X_add_C_eq_zero_iff : p.comp (X + C t) = 0 ↔ p = 0 :=
 lemma comp_X_add_C_ne_zero_iff : p.comp (X + C t) ≠ 0 ↔ p ≠ 0 := comp_X_add_C_eq_zero_iff.not
 
 lemma dvd_comp_C_mul_X_add_C_iff (p q : R[X]) (a b : R) [Invertible a] :
-    p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟ a * (X - C b)) ∣ q := by
+    p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟a * (X - C b)) ∣ q := by
   convert map_dvd_iff <| algEquivCMulXAddC a b using 2
   simp [← comp_eq_aeval, comp_assoc, ← mul_assoc, ← C_mul]
 

Mathlib/Algebra/Polynomial/Laurent.lean

@@ -223,7 +223,7 @@ instance invertibleT (n : ℤ) : Invertible (T n : R[T;T⁻¹]) where
   mul_invOf_self := by rw [← T_add, add_neg_cancel, T_zero]
 
 @[simp]
-theorem invOf_T (n : ℤ) : ⅟ (T n : R[T;T⁻¹]) = T (-n) :=
+theorem invOf_T (n : ℤ) : ⅟(T n : R[T;T⁻¹]) = T (-n) :=
   rfl
 
 theorem isUnit_T (n : ℤ) : IsUnit (T n : R[T;T⁻¹]) :=