OAI/NumberTheory/DirichletL/Hecke/InverseAmplificationRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckeInverseAmplification.SixthFree line 10
2. theorem OAI.SevenEighths.HeckeInverseAmplification.ideal_decomposition_unique line 12
3. abbrev OAI.SevenEighths.HeckeInverseAmplification.FreeRow line 38
4. abbrev OAI.SevenEighths.HeckeInverseAmplification.NonzeroIdeal line 39
5. def OAI.SevenEighths.HeckeInverseAmplification.rowMap line 41
6. theorem OAI.SevenEighths.HeckeInverseAmplification.rowMap_ne_zero line 44
7. theorem OAI.SevenEighths.HeckeInverseAmplification.rowMap_span line 48
8. theorem OAI.SevenEighths.HeckeInverseAmplification.rowMap_injective line 54
9. theorem OAI.SevenEighths.HeckeInverseAmplification.rowMap_norm line 72