Quasigroups

Stream: Is there code for X?

[Yan Yablonovskiy 🇺🇦]

Hey all,

Is there anything like this currently?

import Mathlib.Tactic
import Mathlib.Algebra.Group.Defs
class AssocQuasiGroup.{u} (α : Type u) extends Semigroup α where
latin_sq_prop : ∀a b: α,∃! p:α × α, (a*p.1 = b) ∧ (p.2*a = b)

Based on:
https://en.wikipedia.org/wiki/Quasigroup

[Aaron Liu]

That would be [Semigroup α] [IsLeftCancelMul α] [IsRightCancelMul α]

[Aaron Liu]

Interestingly, we have docs#LeftCancelSemigroup and docs#RightCancelSemigroup but I couldn't find a two-sided version

[Aaron Liu]

hmm after thinking about this a bit more maybe not

[Aaron Liu]

since it doesn't ensure your elements are always "reachable"

[Yan Yablonovskiy 🇺🇦]

Aaron Liu said:

hmm after thinking about this a bit more maybe not

Yea I am a bit worried about the combined uniqueness , and statement of existence.

[Aaron Liu]

in particular any free semigroup satisfies cancellability but you don't get division

[Aaron Liu]

Based on the generality some of the division lemmas are stated in I would guess that this is not in mathlib

[Kenny Lau]

i would additionally advise you to make it data instead of prop