Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

add some docstrings #14

Merged
merged 2 commits into from
Sep 27, 2024
Merged

add some docstrings #14

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cfc9a1a
add some docstrings
Sep 26, 2024
64455ea
Merge branch 'teorth:main' into simple_docstrings
edegeltje Sep 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions equational_theories/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 -/
Expand All @@ -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


Expand Down