OAI/RingTheory/Multiplicity/RootTwist.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.ProjectiveRoot.coefficient_grid_mem line 13
2. lemma OAI.Lech.ProjectiveRoot.coefficient_inverse_grid_mem line 22
3. lemma OAI.Lech.ProjectiveRoot.grid_power_mem line 38
4. lemma OAI.Lech.ProjectiveRoot.coefficient_zpow_grid_mem line 46
5. lemma OAI.Lech.ProjectiveRoot.twist_mem line 69
6. def OAI.Lech.ProjectiveRoot.twistEquiv line 77
7. lemma OAI.Lech.ProjectiveRoot.twistEquiv_val line 97
8. lemma OAI.Lech.ProjectiveRoot.twistEquiv_restriction line 103