OAI/RingTheory/Multiplicity/OrderedRootBasis.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Lech.UniversalSplitting.PowerIndex line 11
2. def OAI.Lech.UniversalSplitting.powerMonomial line 15
3. lemma OAI.Lech.UniversalSplitting.map_powerMonomial line 20
4. theorem OAI.Lech.UniversalSplitting.exists_power_data line 29
5. theorem OAI.Lech.UniversalSplitting.Data.exists_equiv line 141
6. theorem OAI.Lech.UniversalSplitting.Data.exists_power_basis_of_top line 157