Skip to content

Commit bc9337e

Browse files
committed
chore(Ring.Defs): Add docstrings for Semiring and Ring (#9941)
These were lost in the port.
1 parent c60fa7e commit bc9337e

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

Mathlib/Algebra/Ring/Defs.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -137,9 +137,13 @@ class NonAssocRing (α : Type*) extends NonUnitalNonAssocRing α, NonAssocSemiri
137137
AddCommGroupWithOne α
138138
#align non_assoc_ring NonAssocRing
139139

140+
/-- A `Semiring` is a type with addition, multiplication, a `0` and a `1` where addition is
141+
commutative and associative, multiplication is associative and left and right distributive over
142+
addition, and `0` and `1` are additive and multiplicative identities. -/
140143
class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α
141144
#align semiring Semiring
142145

146+
/-- A `Ring` is a `Semiring` with negation making it an additive group. -/
143147
class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
144148
#align ring Ring
145149

0 commit comments

Comments
 (0)