From cfc9a1a9c9801d5a736127229429e3937347410e Mon Sep 17 00:00:00 2001 From: Blizzard_inc Date: Fri, 27 Sep 2024 00:51:21 +0200 Subject: [PATCH] add some docstrings --- equational_theories/Basic.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/equational_theories/Basic.lean b/equational_theories/Basic.lean index 738dc2a5..4fd1cd90 100644 --- a/equational_theories/Basic.lean +++ b/equational_theories/Basic.lean @@ -28,22 +28,30 @@ def Equation4 (G: Type*) [Magma G] := ∀ x y : G, x = x ∘ y /-- The right absorption law -/ def Equation5 (G: Type*) [Magma G] := ∀ x y : G, x = y ∘ x +@[inherit_doc Equation2] def Equation6 (G: Type*) [Magma G] := ∀ x y : G, x = y ∘ y +@[inherit_doc Equation2] def Equation7 (G: Type*) [Magma G] := ∀ x y z : G, x = y ∘ z def Equation8 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ x) +/-- value of multiplication is independent of right argument -/ def Equation38 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = x ∘ y +/-- value of multiplication is independent of left argument; dual of 38 -/ def Equation39 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = y ∘ x +/-- all squares are the same -/ def Equation40 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = y ∘ y +/-- all products are the same -/ def Equation41 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ x = y ∘ z +@[inherit_doc Equation38] def Equation42 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ y = x ∘ z +/-- The commutative law -/ def Equation43 (G: Type*) [Magma G] := ∀ x y : G, x ∘ y = y ∘ x /-- The constant law -/ @@ -61,6 +69,7 @@ def Equation4513 (G: Type*) [Magma G] := ∀ x y z w : G, x ∘ (y ∘ z) = (x def Equation4552 (G: Type*) [Magma G] := ∀ x y z w u : G, x ∘ (y ∘ z) = (x ∘ w) ∘ u +/-- all products of three values are the same, regardless bracketing -/ def Equation4582 (G: Type*) [Magma G] := ∀ x y z w u v: G, x ∘ (y ∘ z) = (w ∘ u) ∘ v