namespace latin:/algebraic ❚

fixmeta latin:/?SFOLEQ ❚

theory BiMagma = 
  include ?Set ❙
  structure add : ?Magma = 
    universe = universe ❙
    U = U ❙
    op # 1 + 2 prec 40 ❙
  ❚
  
  structure mult : ?Magma = 
    universe = universe ❙
    U = U ❙
    op # 1 ⋅ 2 prec 50 ❙
  ❚
❚

theory Ringoid =
  include ?BiMagma ❙
  left_distrib: ⊦ ∀[r]∀[x]∀[y] r⋅(x+y) ≐ r⋅x + r⋅y ❙
  right_distrib: ⊦ ∀[r]∀[x]∀[y] (x+y)⋅r ≐ x⋅r + y⋅r ❙
❚

theory CommRingoid =
  include ?Ringoid ❙
  structure mult : ?CommSemigroup =
    include ?BiMagma/mult ❙
  ❚
❚

theory MonoidalRingoid =
  include ?Ringoid❙
  structure add : ?Monoid = 
    include ?BiMagma?add❙
    elem # zero❙
  ❚
❚

theory BiMonoid =
  include ?MonoidalRingoid❙
  structure mult : ?Monoid = 
    include ?BiMagma?mult❙
    elem # one❙
  ❚
❚

theory NonZeroInvertible =
  include ?BiMonoid❙
  multinverse : ⊦ ∀[x] ¬x≐zero ⇒ ∃[y] mult/inverse x y❙
❚

theory NoZeroDividers =  
  include ?BiMonoid ❙
  no_zero_div: ⊦ ∀[x]∀[y] (x⋅y ≐ zero) ⇒ ((x ≐ zero) ∨ (y ≐ zero)) ❙
❚

theory NonTrivial =
  include ?BiMonoid❙
  neq01: ⊦ ¬(zero ≐ one)❙
❚

theory Semiring = 
	include ?BiMonoid❙
	structure add : ?CommMonoid =                                                                   
	  include ?MonoidalRingoid/add ❙
	❚
❚

theory CommSemiring = 
  include ?Semiring ❙
  include ?CommRingoid ❙
❚

theory NearRing = 
  include ?BiMonoid❙
  structure add : ?Group =
    include ?MonoidalRingoid/add ❙
    inv # - 1 prec 45❙
    div # 1 - 2 prec 40❙
  ❚
❚

theory CommNearRing = 
  include ?NearRing ❙
  include ?CommRingoid ❙
❚

theory Ring = 
  include ?NearRing❙
  // realize ?Semiring❙
  structure add : ?CommGroup =
    include ?NearRing/add ❙
  ❚
❚

theory BooleanRing = 
  include ?Ring ❙
  structure mult : ?IdempotentMonoid =
    include ?BiMonoid/mult❙
  ❚
❚

theory CommRing = 
  include ?Ring ❙
  include ?CommRingoid ❙
❚

theory IntegralDomain =  
  include ?CommRing ❙
  include ?NoZeroDividers❙
❚

theory SkewField = 
  include ?Ring ❙
  include ?NonZeroInvertible❙
  include ?NonTrivial❙
❚

theory Field = 
  include ?SkewField ❙
  include ?CommRingoid ❙
❚

theory BilinearRingoid = 
  include ?Ringoid ❙
  f: U ⟶ U ⟶ U ❙
  bilinear: ⊦ ∀[x]∀[y]∀[z] (f (x+y) z) ≐ (f x z) + (f y z) ∧ (f x (y+z)) ≐ (f x y) + (f y z) ❙
  homogen: ⊦ ∀[r]∀[x]∀[y] f (r⋅x) y ≐ r⋅ (f x y) ∧ f x (r⋅y) ≐ r⋅(f x y) ❙
❚

theory LieRing =
  include ?Ring❙
  include ?BilinearRingoid ❙

  bracket = f ❘# ⟨ 1  2 ⟩ prec 40 ❙ 
  bracket_defn: ⊦ ∀[x]∀[y] ⟨x y⟩ ≐ x⋅y - y⋅x ❙
  jacobi: ⊦ ∀[x]∀[y]∀[z] ⟨x ⟨y z⟩⟩ + ⟨y ⟨z x⟩⟩ + ⟨z ⟨x y⟩⟩ ≐ zero ❙
  alternating: ⊦ ∀[x] ⟨x x⟩ ≐ zero ❙
❚