OAI/RingTheory/DirectFiniteness/OddTorsion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An embedded cyclic subgroup of odd prime order in the prescribed group.

  1. def OAI.KaplanskyCounterexample.Prescription.Output.diagonalPoint line 14
  2. lemma OAI.KaplanskyCounterexample.Prescription.Output.diagonalPoint_injective line 19
  3. def OAI.KaplanskyCounterexample.Prescription.Output.retainedPoint line 23
  4. lemma OAI.KaplanskyCounterexample.Prescription.Output.retainedPoint_injective line 30
  5. theorem OAI.KaplanskyCounterexample.Prescription.Output.prescribed_odd_prime_order line 37