OAI/NumberTheory/PiExponent/LocalAlgebra/LocalIntersectionQuotientTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentJets.W28.LocalIntersection.quotient_cut_length line 11
2. theorem OAI.PiExponentJets.W28.LocalIntersection.quotient_principal_cut_length line 25
3. theorem OAI.PiExponentJets.W28.LocalIntersection.quotient_prime_cut_length line 34
4. def OAI.PiExponentJets.W28.LocalIntersection.quotientMinimalPrimesEquiv line 54
5. theorem OAI.PiExponentJets.W28.LocalIntersection.quotientMinimalPrimesEquiv_apply line 73
6. theorem OAI.PiExponentJets.W28.LocalIntersection.quotient_minimal_local_length line 77