OAI/NumberTheory/DirichletL/Descent/SecondWholeMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.actualSecondChild_outer_units line 13
2. theorem OAI.SevenEighths.InverseMoment.actualSecondChild_label_units line 17
3. theorem OAI.SevenEighths.InverseMoment.actualSecondTriples_units line 21
4. theorem OAI.SevenEighths.InverseMoment.assigned_second_triples_subset line 25
5. theorem OAI.SevenEighths.InverseMoment.assigned_second_mass_le_original line 35