OAI/NumberTheory/PiExponent/LocalAlgebra/RetainedMinimalPrimeFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentJets.W22.RetainedMinimalPrime line 15
2. instance OAI.PiExponentJets.W22.RetainedMinimalPrime.finiteFamily line 22
3. instance OAI.PiExponentJets.W22.RetainedMinimalPrime.(instance at line 29) line 29
4. def OAI.PiExponentJets.W22.RetainedMinimalPrime.toComponent line 31
5. theorem OAI.PiExponentJets.W22.RetainedMinimalPrime.toComponent_val line 40
6. theorem OAI.PiExponentJets.W22.RetainedMinimalPrime.toComponent_injective line 46
7. def OAI.PiExponentJets.W22.RetainedPrimeCycle.canonicalRetainedCut line 57
8. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.canonicalRetainedCut_covers line 86
9. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.canonicalRetainedCut_next_le_target line 100