OAI/RingTheory/Multiplicity/RootBaseProjective.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.ProjectiveScalar.trans line 13
2. def OAI.Lech.ProjectiveRoot.baseBasisEquiv line 30
3. lemma OAI.Lech.ProjectiveRoot.ring_base_free line 37
4. lemma OAI.Lech.ProjectiveRoot.sections_base_projective line 40