OAI/RingTheory/DirectFiniteness/PrescribedPresentation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite presentation of the prescribed group.

  1. lemma OAI.KaplanskyCounterexample.Prescription.Output.prescribed_base_finitelyPresented line 15
  2. theorem OAI.KaplanskyCounterexample.Prescription.Output.prescribed_finitelyPresented line 21