[Merged by Bors] - feat: port Algebra.Ring.Defs

Mathlib.lean

@@ -19,6 +19,7 @@ import Mathlib.Algebra.Order.Monoid.Lemmas
 import Mathlib.Algebra.Order.Ring
 import Mathlib.Algebra.PEmptyInstances
 import Mathlib.Algebra.Ring.Basic
+import Mathlib.Algebra.Ring.Defs
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
 import Mathlib.Control.Random
 import Mathlib.Control.ULift

Mathlib/Algebra/Group/Defs.lean

@@ -112,11 +112,13 @@ end Mul
 /-- A semigroup is a type with an associative `(*)`. -/
 @[ext]
 class Semigroup (G : Type u) extends Mul G where
+  /-- Multiplication is associative -/
   mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
 
 /-- An additive semigroup is a type with an associative `(+)`. -/
 @[ext]
 class AddSemigroup (G : Type u) extends Add G where
+  /-- Addition is associative -/
   add_assoc : ∀ a b c : G, a + b + c = a + (b + c)
 
 attribute [to_additive] Semigroup
@@ -234,13 +236,17 @@ end RightCancelSemigroup
 /-- Typeclass for expressing that a type `M` with multiplication and a one satisfies
 `1 * a = a` and `a * 1 = a` for all `a : M`. -/
 class MulOneClass (M : Type u) extends One M, Mul M where
+  /-- One is a left neutral element for multiplication -/
   one_mul : ∀ a : M, 1 * a = a
+  /-- One is a right neutral element for multiplication -/
   mul_one : ∀ a : M, a * 1 = a
 
 /-- Typeclass for expressing that a type `M` with addition and a zero satisfies
 `0 + a = a` and `a + 0 = a` for all `a : M`. -/
 class AddZeroClass (M : Type u) extends Zero M, Add M where
+  /-- Zero is a left neutral element for addition -/
   zero_add : ∀ a : M, 0 + a = a
+  /-- Zero is a right neutral element for addition -/
   add_zero : ∀ a : M, a + 0 = a
 
 attribute [to_additive] MulOneClass

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -41,7 +41,9 @@ Monoid.npow_succ'
 /-- Typeclass for expressing that a type `M₀` with multiplication and a zero satisfies
 `0 * a = 0` and `a * 0 = 0` for all `a : M₀`. -/
 class MulZeroClass (M₀ : Type u) extends Mul M₀, Zero M₀ where
+  /-- Zero is a left absorbing element for multiplication -/
   zero_mul : ∀ a : M₀, 0 * a = 0
+  /-- Zero is a right absorbing element for multiplication -/
   mul_zero : ∀ a : M₀, a * 0 = 0
 
 export MulZeroClass (zero_mul mul_zero)

Mathlib/Algebra/Ring/Basic.lean

@@ -2,37 +2,15 @@ import Mathlib.Algebra.Group.Commute
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Tactic.Spread
+import Mathlib.Algebra.Ring.Defs
 
 /-
 # Semirings and rings
 -/
 
-/-- A typeclass stating that multiplication is left and right distributive
-over addition. -/
-class Distrib (R : Type u) extends Mul R, Add R where
-  left_distrib : ∀ a b c : R, a * (b + c) = (a * b) + (a * c)
-  right_distrib : ∀ a b c : R, (a + b) * c = (a * c) + (b * c)
 
 export Distrib (left_distrib right_distrib)
 
-section
-variable {R} [Distrib R]
-theorem mul_add (a b c : R) : a * (b + c) = a * b + a * c := Distrib.left_distrib a b c
-theorem add_mul (a b c : R) : (a + b) * c = a * c + b * c := Distrib.right_distrib a b c
-end
-
-/-- A not-necessarily-unital, not-necessarily-associative semiring. -/
-class NonUnitalNonAssocSemiring (R : Type u) extends
-  AddCommMonoid R, Distrib R, MulZeroClass R, AddMonoidWithOne R
-
-/-- An associative but not-necessarily unital semiring. -/
-class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α
-
-/-- A unital but not-necessarily-associative semiring. -/
-class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α
-
-class Semiring (R : Type u) extends NonUnitalSemiring R, NonAssocSemiring R, MonoidWithZero R
-
 section Semiring
 
 -- TODO: put these in the right place
@@ -65,28 +43,8 @@ theorem Nat.cast_commute [Semiring α] (n : ℕ) (x : α) : Commute (↑n) x :=
 
 end Semiring
 
-class CommSemiring (R : Type u) extends Semiring R, CommMonoid R where
-  -- TODO: doesn't work
-  right_distrib a b c := (by rw [mul_comm, mul_add, mul_comm c, mul_comm c])
-
-class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
-
 example [Ring R] : HasInvolutiveNeg R := inferInstance
 
-@[simp] theorem neg_mul {R} [Ring R] (a b : R) : (-a) * b = -(a * b) :=
-  eq_of_sub_eq_zero' <| by rw [sub_eq_add_neg, neg_neg, ← add_mul, neg_add_self, zero_mul]
-
-@[simp] lemma mul_neg [Ring R] (a b : R) : a * -b = - (a * b) :=
-  eq_of_sub_eq_zero' <| by rw [sub_eq_add_neg, neg_neg, ← mul_add, neg_add_self, mul_zero]
-
-theorem neg_mul_eq_neg_mul {R} [Ring R] (a b : R) : -(a * b) = (-a) * b := (neg_mul ..).symm
-
-theorem mul_sub_right_distrib [Ring R] (a b c : R) : (a - b) * c = a * c - b * c := by
-  simpa only [sub_eq_add_neg, neg_mul_eq_neg_mul] using add_mul a (-b) c
-
-alias mul_sub_right_distrib ← sub_mul
-
-class CommRing (R : Type u) extends Ring R, CommSemiring R
 
 /- Instances -/