OAI/NumberTheory/PiExponent/LocalAlgebra/GlobalInvertibleIdeal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.InvertibleLocal.restricted_image_on_chart line 13
2. theorem OAI.PiExponentSeshadri.InvertibleLocal.mono_iso_inv_comp line 39

   Also declared: OAI/NumberTheory/PiExponent/LocalAlgebra/InvertibleIdealLocal.lean:62 (same declaration text).

3. lemma OAI.PiExponentSeshadri.InvertibleLocal.local_equation_on_chart line 42
4. lemma OAI.PiExponentSeshadri.InvertibleLocal.local_equations line 70
5. lemma OAI.PiExponentSeshadri.InvertibleLocal.invertible_iff_local_equations line 83
6. lemma OAI.PiExponentSeshadri.InvertibleLocal.invertible_congr line 90
7. lemma OAI.PiExponentSeshadri.InvertibleLocal.presents_restrict_general line 101
8. lemma OAI.PiExponentSeshadri.InvertibleLocal.invertible_restrict_general line 114
9. lemma OAI.PiExponentSeshadri.InvertibleLocal.invertible_of_cover line 121