OAI/RingTheory/Multiplicity/AlgebraicResidueTensor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.ResidueTensor.fiberEquiv line 13
2. lemma OAI.Lech.ResidueTensor.fiberEquiv_includeRight line 18
3. lemma OAI.Lech.ResidueTensor.residue_surjective line 29
4. lemma OAI.Lech.ResidueTensor.maximal_map line 43
5. lemma OAI.Lech.ResidueTensor.isLocal line 47
6. lemma OAI.Lech.ResidueTensor.maximalIdeal_eq_map line 61