chore(*): Use non-greek variable names here and there (#17035)

... for monoids, rings, and fields.

Mathlib/Algebra/Associated/OrderedCommMonoid.lean

@@ -23,14 +23,14 @@ Then we show that the quotient type `Associates` is a monoid
 and prove basic properties of this quotient.
 -/
 
-variable {α : Type*} [CancelCommMonoidWithZero α]
+variable {M : Type*} [CancelCommMonoidWithZero M]
 
 namespace Associates
 
-instance instOrderedCommMonoid : OrderedCommMonoid (Associates α) where
-  mul_le_mul_left := fun a _ ⟨d, hd⟩ c => hd.symm ▸ mul_assoc c a d ▸ le_mul_right (α := α)
+instance instOrderedCommMonoid : OrderedCommMonoid (Associates M) where
+  mul_le_mul_left := fun a _ ⟨d, hd⟩ c => hd.symm ▸ mul_assoc c a d ▸ le_mul_right
 
-instance : CanonicallyOrderedCommMonoid (Associates α) where
+instance : CanonicallyOrderedCommMonoid (Associates M) where
   exists_mul_of_le h := h
   le_self_mul _ b := ⟨b, rfl⟩
   bot_le _ := one_le

Mathlib/Algebra/Field/Basic.lean

@@ -18,16 +18,16 @@ open Function OrderDual Set
 
 universe u
 
-variable {α β K : Type*}
+variable {K L : Type*}
 
 section DivisionSemiring
 
-variable [DivisionSemiring α] {a b c d : α}
+variable [DivisionSemiring K] {a b c d : K}
 
-theorem add_div (a b c : α) : (a + b) / c = a / c + b / c := by simp_rw [div_eq_mul_inv, add_mul]
+theorem add_div (a b c : K) : (a + b) / c = a / c + b / c := by simp_rw [div_eq_mul_inv, add_mul]
 
 @[field_simps]
-theorem div_add_div_same (a b c : α) : a / c + b / c = (a + b) / c :=
+theorem div_add_div_same (a b c : K) : a / c + b / c = (a + b) / c :=
   (add_div _ _ _).symm
 
 theorem same_add_div (h : b ≠ 0) : (b + a) / b = 1 + a / b := by rw [← div_self h, add_div]
@@ -49,15 +49,15 @@ theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div (ha : a ≠ 0) (hb :
     1 / a * (a + b) * (1 / b) = 1 / a + 1 / b := by
   simpa only [one_div] using (inv_add_inv' ha hb).symm
 
-theorem add_div_eq_mul_add_div (a b : α) (hc : c ≠ 0) : a + b / c = (a * c + b) / c :=
+theorem add_div_eq_mul_add_div (a b : K) (hc : c ≠ 0) : a + b / c = (a * c + b) / c :=
   (eq_div_iff_mul_eq hc).2 <| by rw [right_distrib, div_mul_cancel₀ _ hc]
 
 @[field_simps]
-theorem add_div' (a b c : α) (hc : c ≠ 0) : b + a / c = (b * c + a) / c := by
+theorem add_div' (a b c : K) (hc : c ≠ 0) : b + a / c = (b * c + a) / c := by
   rw [add_div, mul_div_cancel_right₀ _ hc]
 
 @[field_simps]
-theorem div_add' (a b c : α) (hc : c ≠ 0) : a / c + b = (a + b * c) / c := by
+theorem div_add' (a b c : K) (hc : c ≠ 0) : a / c + b = (a + b * c) / c := by
   rwa [add_comm, add_div', add_comm]
 
 protected theorem Commute.div_add_div (hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0)
@@ -167,9 +167,9 @@ end DivisionRing
 
 section Semifield
 
-variable [Semifield α] {a b c d : α}
+variable [Semifield K] {a b c d : K}
 
-theorem div_add_div (a : α) (c : α) (hb : b ≠ 0) (hd : d ≠ 0) :
+theorem div_add_div (a : K) (c : K) (hb : b ≠ 0) (hd : d ≠ 0) :
     a / b + c / d = (a * d + b * c) / (b * d) :=
   (Commute.all b _).div_add_div (Commute.all _ _) hb hd
 
@@ -211,7 +211,7 @@ end Field
 
 namespace RingHom
 
-protected theorem injective [DivisionRing α] [Semiring β] [Nontrivial β] (f : α →+* β) :
+protected theorem injective [DivisionRing K] [Semiring L] [Nontrivial L] (f : K →+* L) :
     Injective f :=
   (injective_iff_map_eq_zero f).2 fun _ ↦ (map_eq_zero f).1
 
@@ -242,18 +242,18 @@ noncomputable abbrev Field.ofIsUnitOrEqZero [CommRing R] (h : ∀ a : R, IsUnit
 end NoncomputableDefs
 
 namespace Function.Injective
-variable [Zero α] [Add α] [Neg α] [Sub α] [One α] [Mul α] [Inv α] [Div α] [SMul ℕ α] [SMul ℤ α]
-  [SMul ℚ≥0 α] [SMul ℚ α] [Pow α ℕ] [Pow α ℤ] [NatCast α] [IntCast α] [NNRatCast α] [RatCast α]
-  (f : α → β) (hf : Injective f)
+variable [Zero K] [Add K] [Neg K] [Sub K] [One K] [Mul K] [Inv K] [Div K] [SMul ℕ K] [SMul ℤ K]
+  [SMul ℚ≥0 K] [SMul ℚ K] [Pow K ℕ] [Pow K ℤ] [NatCast K] [IntCast K] [NNRatCast K] [RatCast K]
+  (f : K → L) (hf : Injective f)
 
 /-- Pullback a `DivisionSemiring` along an injective function. -/
 -- See note [reducible non-instances]
-protected abbrev divisionSemiring [DivisionSemiring β] (zero : f 0 = 0) (one : f 1 = 1)
+protected abbrev divisionSemiring [DivisionSemiring L] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
     (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : DivisionSemiring α where
+    (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : DivisionSemiring K where
   toSemiring := hf.semiring f zero one add mul nsmul npow natCast
   __ := hf.groupWithZero f zero one mul inv div npow zpow
   nnratCast_def q := hf <| by rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
@@ -262,15 +262,15 @@ protected abbrev divisionSemiring [DivisionSemiring β] (zero : f 0 = 0) (one :
 
 /-- Pullback a `DivisionSemiring` along an injective function. -/
 -- See note [reducible non-instances]
-protected abbrev divisionRing [DivisionRing β] (zero : f 0 = 0) (one : f 1 = 1)
+protected abbrev divisionRing [DivisionRing L] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
     (div : ∀ x y, f (x / y) = f x / f y)
     (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
     (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
     (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q)
-    (ratCast : ∀ q : ℚ, f q = q) : DivisionRing α where
+    (ratCast : ∀ q : ℚ, f q = q) : DivisionRing K where
   toRing := hf.ring f zero one add mul neg sub nsmul zsmul npow natCast intCast
   __ := hf.groupWithZero f zero one mul inv div npow zpow
   __ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
@@ -280,19 +280,19 @@ protected abbrev divisionRing [DivisionRing β] (zero : f 0 = 0) (one : f 1 = 1)
 
 /-- Pullback a `Field` along an injective function. -/
 -- See note [reducible non-instances]
-protected abbrev semifield [Semifield β] (zero : f 0 = 0) (one : f 1 = 1)
+protected abbrev semifield [Semifield L] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
     (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : Semifield α where
+    (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : Semifield K where
   toCommSemiring := hf.commSemiring f zero one add mul nsmul npow natCast
   __ := hf.commGroupWithZero f zero one mul inv div npow zpow
   __ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
 
 /-- Pullback a `Field` along an injective function. -/
 -- See note [reducible non-instances]
-protected abbrev field [Field β] (zero : f 0 = 0) (one : f 1 = 1)
+protected abbrev field [Field L] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
     (div : ∀ x y, f (x / y) = f x / f y)
@@ -301,7 +301,7 @@ protected abbrev field [Field β] (zero : f 0 = 0) (one : f 1 = 1)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
     (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q)
     (ratCast : ∀ q : ℚ, f q = q) :
-    Field α where
+    Field K where
   toCommRing := hf.commRing f zero one add mul neg sub nsmul zsmul npow natCast intCast
   __ := hf.divisionRing f zero one add mul neg sub inv div nsmul zsmul nnqsmul qsmul npow zpow
     natCast intCast nnratCast ratCast
@@ -312,30 +312,30 @@ end Function.Injective
 
 namespace OrderDual
 
-instance instRatCast [RatCast α] : RatCast αᵒᵈ := ‹_›
-instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵒᵈ := ‹_›
-instance instDivisionRing [DivisionRing α] : DivisionRing αᵒᵈ := ‹_›
-instance instSemifield [Semifield α] : Semifield αᵒᵈ := ‹_›
-instance instField [Field α] : Field αᵒᵈ := ‹_›
+instance instRatCast [RatCast K] : RatCast Kᵒᵈ := ‹_›
+instance instDivisionSemiring [DivisionSemiring K] : DivisionSemiring Kᵒᵈ := ‹_›
+instance instDivisionRing [DivisionRing K] : DivisionRing Kᵒᵈ := ‹_›
+instance instSemifield [Semifield K] : Semifield Kᵒᵈ := ‹_›
+instance instField [Field K] : Field Kᵒᵈ := ‹_›
 
 end OrderDual
 
-@[simp] lemma toDual_ratCast [RatCast α] (n : ℚ) : toDual (n : α) = n := rfl
+@[simp] lemma toDual_ratCast [RatCast K] (n : ℚ) : toDual (n : K) = n := rfl
 
-@[simp] lemma ofDual_ratCast [RatCast α] (n : ℚ) : (ofDual n : α) = n := rfl
+@[simp] lemma ofDual_ratCast [RatCast K] (n : ℚ) : (ofDual n : K) = n := rfl
 
 /-! ### Lexicographic order -/
 
 namespace Lex
 
-instance instRatCast [RatCast α] : RatCast (Lex α) := ‹_›
-instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring (Lex α) := ‹_›
-instance instDivisionRing [DivisionRing α] : DivisionRing (Lex α) := ‹_›
-instance instSemifield [Semifield α] : Semifield (Lex α) := ‹_›
-instance instField [Field α] : Field (Lex α) := ‹_›
+instance instRatCast [RatCast K] : RatCast (Lex K) := ‹_›
+instance instDivisionSemiring [DivisionSemiring K] : DivisionSemiring (Lex K) := ‹_›
+instance instDivisionRing [DivisionRing K] : DivisionRing (Lex K) := ‹_›
+instance instSemifield [Semifield K] : Semifield (Lex K) := ‹_›
+instance instField [Field K] : Field (Lex K) := ‹_›
 
 end Lex
 
-@[simp] lemma toLex_ratCast [RatCast α] (n : ℚ) : toLex (n : α) = n := rfl
+@[simp] lemma toLex_ratCast [RatCast K] (n : ℚ) : toLex (n : K) = n := rfl
 
-@[simp] lemma ofLex_ratCast [RatCast α] (n : ℚ) : (ofLex n : α) = n := rfl
+@[simp] lemma ofLex_ratCast [RatCast K] (n : ℚ) : (ofLex n : K) = n := rfl

Mathlib/Algebra/Field/Defs.lean

@@ -54,7 +54,7 @@ open Function Set
 
 universe u
 
-variable {α β K : Type*}
+variable {K : Type*}
 
 /-- The default definition of the coercion `ℚ≥0 → K` for a division semiring `K`.
 
@@ -81,23 +81,23 @@ itself). See also note [forgetful inheritance].
 
 If the division semiring has positive characteristic `p`, our division by zero convention forces
 `nnratCast (1 / p) = 1 / 0 = 0`. -/
-class DivisionSemiring (α : Type*) extends Semiring α, GroupWithZero α, NNRatCast α where
+class DivisionSemiring (K : Type*) extends Semiring K, GroupWithZero K, NNRatCast K where
   protected nnratCast := NNRat.castRec
   /-- However `NNRat.cast` is defined, it must be propositionally equal to `a / b`.
 
   Do not use this lemma directly. Use `NNRat.cast_def` instead. -/
-  protected nnratCast_def (q : ℚ≥0) : (NNRat.cast q : α) = q.num / q.den := by intros; rfl
+  protected nnratCast_def (q : ℚ≥0) : (NNRat.cast q : K) = q.num / q.den := by intros; rfl
   /-- Scalar multiplication by a nonnegative rational number.
 
   Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
   `nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.
 
   Do not use directly. Instead use the `•` notation. -/
-  protected nnqsmul : ℚ≥0 → α → α
+  protected nnqsmul : ℚ≥0 → K → K
   /-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.
 
   Do not use this lemma directly. Use `NNRat.smul_def` instead. -/
-  protected nnqsmul_def (q : ℚ≥0) (a : α) : nnqsmul q a = NNRat.cast q * a := by intros; rfl
+  protected nnqsmul_def (q : ℚ≥0) (a : K) : nnqsmul q a = NNRat.cast q * a := by intros; rfl
 
 /-- A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.
 
@@ -109,48 +109,48 @@ See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ
 
 If the division ring has positive characteristic `p`, our division by zero convention forces
 `ratCast (1 / p) = 1 / 0 = 0`. -/
-class DivisionRing (α : Type*)
-  extends Ring α, DivInvMonoid α, Nontrivial α, NNRatCast α, RatCast α where
+class DivisionRing (K : Type*)
+  extends Ring K, DivInvMonoid K, Nontrivial K, NNRatCast K, RatCast K where
   /-- For a nonzero `a`, `a⁻¹` is a right multiplicative inverse. -/
-  protected mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
+  protected mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1
   /-- The inverse of `0` is `0` by convention. -/
-  protected inv_zero : (0 : α)⁻¹ = 0
+  protected inv_zero : (0 : K)⁻¹ = 0
   protected nnratCast := NNRat.castRec
   /-- However `NNRat.cast` is defined, it must be equal to `a / b`.
 
   Do not use this lemma directly. Use `NNRat.cast_def` instead. -/
-  protected nnratCast_def (q : ℚ≥0) : (NNRat.cast q : α) = q.num / q.den := by intros; rfl
+  protected nnratCast_def (q : ℚ≥0) : (NNRat.cast q : K) = q.num / q.den := by intros; rfl
   /-- Scalar multiplication by a nonnegative rational number.
 
   Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
   `nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.
 
   Do not use directly. Instead use the `•` notation. -/
-  protected nnqsmul : ℚ≥0 → α → α
+  protected nnqsmul : ℚ≥0 → K → K
   /-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.
 
   Do not use this lemma directly. Use `NNRat.smul_def` instead. -/
-  protected nnqsmul_def (q : ℚ≥0) (a : α) : nnqsmul q a = NNRat.cast q * a := by intros; rfl
+  protected nnqsmul_def (q : ℚ≥0) (a : K) : nnqsmul q a = NNRat.cast q * a := by intros; rfl
   protected ratCast := Rat.castRec
   /-- However `Rat.cast q` is defined, it must be propositionally equal to `q.num / q.den`.
 
   Do not use this lemma directly. Use `Rat.cast_def` instead. -/
-  protected ratCast_def (q : ℚ) : (Rat.cast q : α) = q.num / q.den := by intros; rfl
+  protected ratCast_def (q : ℚ) : (Rat.cast q : K) = q.num / q.den := by intros; rfl
   /-- Scalar multiplication by a rational number.
 
   Unless there is a risk of a `Module ℚ _` instance diamond, write `qsmul := _`. This will set
   `qsmul` to `(Rat.cast · * ·)` thanks to unification in the default proof of `qsmul_def`.
 
   Do not use directly. Instead use the `•` notation. -/
-  protected qsmul : ℚ → α → α
+  protected qsmul : ℚ → K → K
   /-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.
 
   Do not use this lemma directly. Use `Rat.cast_def` instead. -/
-  protected qsmul_def (a : ℚ) (x : α) : qsmul a x = Rat.cast a * x := by intros; rfl
+  protected qsmul_def (a : ℚ) (x : K) : qsmul a x = Rat.cast a * x := by intros; rfl
 
 -- see Note [lower instance priority]
-instance (priority := 100) DivisionRing.toDivisionSemiring [DivisionRing α] : DivisionSemiring α :=
-  { ‹DivisionRing α› with }
+instance (priority := 100) DivisionRing.toDivisionSemiring [DivisionRing K] : DivisionSemiring K :=
+  { ‹DivisionRing K› with }
 
 /-- A `Semifield` is a `CommSemiring` with multiplicative inverses for nonzero elements.
 
@@ -161,7 +161,7 @@ itself). See also note [forgetful inheritance].
 
 If the semifield has positive characteristic `p`, our division by zero convention forces
 `nnratCast (1 / p) = 1 / 0 = 0`. -/
-class Semifield (α : Type*) extends CommSemiring α, DivisionSemiring α, CommGroupWithZero α
+class Semifield (K : Type*) extends CommSemiring K, DivisionSemiring K, CommGroupWithZero K
 
 /-- A `Field` is a `CommRing` with multiplicative inverses for nonzero elements.
 
@@ -175,19 +175,19 @@ If the field has positive characteristic `p`, our division by zero convention fo
 class Field (K : Type u) extends CommRing K, DivisionRing K
 
 -- see Note [lower instance priority]
-instance (priority := 100) Field.toSemifield [Field α] : Semifield α := { ‹Field α› with }
+instance (priority := 100) Field.toSemifield [Field K] : Semifield K := { ‹Field K› with }
 
 namespace NNRat
-variable [DivisionSemiring α]
+variable [DivisionSemiring K]
 
-instance (priority := 100) smulDivisionSemiring : SMul ℚ≥0 α := ⟨DivisionSemiring.nnqsmul⟩
+instance (priority := 100) smulDivisionSemiring : SMul ℚ≥0 K := ⟨DivisionSemiring.nnqsmul⟩
 
-lemma cast_def (q : ℚ≥0) : (q : α) = q.num / q.den := DivisionSemiring.nnratCast_def _
-lemma smul_def (q : ℚ≥0) (a : α) : q • a = q * a := DivisionSemiring.nnqsmul_def q a
+lemma cast_def (q : ℚ≥0) : (q : K) = q.num / q.den := DivisionSemiring.nnratCast_def _
+lemma smul_def (q : ℚ≥0) (a : K) : q • a = q * a := DivisionSemiring.nnqsmul_def q a
 
-variable (α)
+variable (K)
 
-@[simp] lemma smul_one_eq_cast (q : ℚ≥0) : q • (1 : α) = q := by rw [NNRat.smul_def, mul_one]
+@[simp] lemma smul_one_eq_cast (q : ℚ≥0) : q • (1 : K) = q := by rw [NNRat.smul_def, mul_one]
 
 @[deprecated (since := "2024-05-03")] alias smul_one_eq_coe := smul_one_eq_cast