From b4dda71e1bd8297df387af10ff0ca7f0a5127385 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 23 Sep 2024 08:50:51 +0000 Subject: [PATCH] chore(*): Use non-greek variable names here and there (#17035) ... for monoids, rings, and fields. --- .../Algebra/Associated/OrderedCommMonoid.lean | 8 +-- Mathlib/Algebra/Field/Basic.lean | 70 +++++++++---------- Mathlib/Algebra/Field/Defs.lean | 50 ++++++------- 3 files changed, 64 insertions(+), 64 deletions(-) diff --git a/Mathlib/Algebra/Associated/OrderedCommMonoid.lean b/Mathlib/Algebra/Associated/OrderedCommMonoid.lean index 16c1b23b72bf2..ab1745e4359de 100644 --- a/Mathlib/Algebra/Associated/OrderedCommMonoid.lean +++ b/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 diff --git a/Mathlib/Algebra/Field/Basic.lean b/Mathlib/Algebra/Field/Basic.lean index fa1a788fb74a7..570a5278b9b56 100644 --- a/Mathlib/Algebra/Field/Basic.lean +++ b/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,7 +262,7 @@ 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) @@ -270,7 +270,7 @@ protected abbrev divisionRing [DivisionRing β] (zero : f 0 = 0) (one : f 1 = 1) (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 diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean index 4943b798adf4c..834f25d5fc450 100644 --- a/Mathlib/Algebra/Field/Defs.lean +++ b/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