OAI/RingTheory/Multiplicity/RootUlrichModule.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.ModuleDescent.exists_basis_of_baseChange line 14
2. lemma OAI.Lech.RootInvariants.homogeneous_product_member line 52
3. def OAI.Lech.RootInvariants.homogeneousSection line 75
4. def OAI.Lech.RootInvariants.consecutiveSection line 80
5. lemma OAI.Lech.RootInvariants.tensorEquiv_one_tmul line 86
6. theorem OAI.Lech.RootInvariants.exists_consecutive_basis line 93