OAI/NumberTheory/DirichletL/Descent/GeneratorTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.secondChildColumn_label_transfer line 16
2. theorem OAI.SevenEighths.InverseMoment.secondChildColumn_puncture_unit line 24
3. theorem OAI.SevenEighths.InverseMoment.secondChildColumn_generator_unit line 32
4. theorem OAI.SevenEighths.InverseMoment.finiteCanonicalMarkedRow_label_transfer line 41
5. theorem OAI.SevenEighths.InverseMoment.generator_eq_unit_primary line 48
6. lemma OAI.SevenEighths.InverseMoment.normalized_generator_row_norm line 56