OAI/NumberTheory/Ostmann/Characters/TemplatePivotUnits.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Characters.Template.signedChildFrequencyline 10 - theorem
OAI.Ostmann.Characters.Template.primeRowUnits_oppositeline 13 - theorem
OAI.Ostmann.Characters.Template.reversal_copied_residueline 25 - theorem
OAI.Ostmann.Characters.Template.reversal_root_residue_ne_zeroline 39 - theorem
OAI.Ostmann.Characters.Template.reversal_pivot_unitsline 54