Lean 4 på svenska

Den algebraiska hierarkin från magmor till abelska grupper uttryckt i Lean med hjälp av Mathlib.

import Mathlib
noncomputable section
set_option autoImplicit false

-- Magma (multiplikativ, *)
class Magma (P : Type*) extends Mul P
instance (P : Type*) [Mul P] : Magma P := {}

-- Magma (additiv, +)
class AddMagma (P : Type*) extends Add P
instance (P : Type*) [Add P] : AddMagma P := {}

-- Hierarki:
-- * Magma https://sv.wikipedia.org/wiki/Magma_(matematik)
-- * Semigrupp, https://sv.wikipedia.org/wiki/Semigrupp
-- * Monoid, https://sv.wikipedia.org/wiki/Monoid
-- * Grupp, https://sv.wikipedia.org/wiki/Grupp_(matematik)
-- * Kommutativ grupp eller abelsk grupp, https://sv.wikipedia.org/wiki/Abelsk_grupp

-- En semigrupp är en magma.
example (g : Type) [Semigroup g] : Magma g := by infer_instance
-- En monoid är en semigrupp.
example (g : Type) [Monoid g] : Semigroup g := by infer_instance
-- En grupp är en monoid.
example (g : Type) [Group g] : Monoid g := by infer_instance
-- En kommutativ grupp (abelsk grupp) är en grupp.
example (g : Type) [CommGroup g] : Group g := by infer_instance

-- Motsvarande additiva struktur:
example (g : Type) [AddSemigroup g] : AddMagma g := by infer_instance
example (g : Type) [AddMonoid g] : AddSemigroup g := by infer_instance
example (g : Type) [AddGroup g] : AddMonoid g := by infer_instance
example (g : Type) [AddCommGroup g] : AddGroup g := by infer_instance