OAI/NumberTheory/PiExponent/LocalAlgebra/LocalIntersectionFormula.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PiExponentJets.W28.LocalIntersection.minimalPrimeCutSum_quotientline 11 - theorem
OAI.PiExponentJets.W28.LocalIntersection.quotient_parameter_mem_nonZeroDivisorsline 34 - theorem
OAI.PiExponentJets.W28.LocalIntersection.local_onecut_lengthline 44 - theorem
OAI.PiExponentJets.W28.LocalIntersection.localOneCutLengthStatement_provedline 66