OAI/NumberTheory/PrimePackets/AdelicFlow.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PrimeDegreePackets.Adelic.splitFlowline 11 - lemma
OAI.PrimeDegreePackets.Adelic.continuous_splitFlowline 14 - lemma
OAI.PrimeDegreePackets.Adelic.diagonalUnits_splitFlowline 17 - def
OAI.PrimeDegreePackets.Adelic.flowIdeleline 25 - def
OAI.PrimeDegreePackets.Adelic.flowTorusline 29 - lemma
OAI.PrimeDegreePackets.Adelic.continuous_flowTorusline 33 - lemma
OAI.PrimeDegreePackets.Adelic.adelicIdelePoint_flowline 38 - lemma
OAI.PrimeDegreePackets.Adelic.adelicTorusPoint_flowline 61