OAI/NumberTheory/DirichletL/Descent/SecondModeCanonical.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.InverseMoment.secondInheritedProfileline 18 - def
OAI.SevenEighths.InverseMoment.secondModeLeftline 22 - def
OAI.SevenEighths.InverseMoment.secondModeRightline 29 - def
OAI.SevenEighths.InverseMoment.secondModeOuterline 37 - def
OAI.SevenEighths.InverseMoment.secondModeBranchline 43 - theorem
OAI.SevenEighths.InverseMoment.second_inherited_mode_canonicalline 53 - theorem
OAI.SevenEighths.InverseMoment.actual_second_modes_common_sectorsline 72