OAI/NumberTheory/DirichletL/Reflection/ChoiceTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseReflectedPhase.fixedTupleFamily line 13
2. lemma OAI.SevenEighths.InverseReflectedPhase.fixedTupleFamily_at_choice line 21
3. def OAI.SevenEighths.InverseReflectedPhase.fixedTupleCoefficient line 33
4. lemma OAI.SevenEighths.InverseReflectedPhase.fixedTupleCoefficient_at line 37
5. lemma OAI.SevenEighths.InverseReflectedPhase.fixedTupleCoefficient_norm line 42
6. def OAI.SevenEighths.InverseReflectedPhase.activeChoiceControlled line 60
7. lemma OAI.SevenEighths.InverseReflectedPhase.activeChoiceControlled_value line 67
8. theorem OAI.SevenEighths.InverseReflectedPhase.literalWholeRow_eq_original_choices line 81