• 1 Green’s Relations ▶
    • 1.1 Equivalences from Preorders
    • 1.2 Green’s Equivalences (\(\mathcal R, \mathcal L, \mathcal J, \mathcal H\))
    • 1.3 Basic Preorder Properties
    • 1.4 R–L multiplicative compatibility
    • 1.5 R–L commutativity
    • 1.6 The D-equivalence
    • 1.7 Equivalence classes
  • 2 Location Theorem ▶
    • 2.1 Green’s Lemma
    • 2.2 Location Theorem (Proposition 1.6)
  • Dependency graph

My formalization project

Howard Straubing, Soleil Repple, Ayden Lamparski, Nathan Hartdog

  • 1 Green’s Relations
    • 1.1 Equivalences from Preorders
    • 1.2 Green’s Equivalences (\(\mathcal R, \mathcal L, \mathcal J, \mathcal H\))
    • 1.3 Basic Preorder Properties
    • 1.4 R–L multiplicative compatibility
    • 1.5 R–L commutativity
    • 1.6 The D-equivalence
    • 1.7 Equivalence classes
  • 2 Location Theorem
    • 2.1 Green’s Lemma
    • 2.2 Location Theorem (Proposition 1.6)