OAI/RingTheory/DirectFiniteness/FinitePresentation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite presentations of finite-relation quotients and products.

  1. lemma OAI.KaplanskyCounterexample.CurrentMain.finitelyPresented_fg line 13
  2. lemma OAI.KaplanskyCounterexample.CurrentMain.conGen_ker_finite line 18
  3. lemma OAI.KaplanskyCounterexample.CurrentMain.finitelyPresented_finite_relations line 45
  4. lemma OAI.KaplanskyCounterexample.CurrentMain.commuting_of_generators line 50
  5. lemma OAI.KaplanskyCounterexample.CurrentMain.finitelyPresented_prod line 68