OAI/NumberTheory/PiExponent/LocalAlgebra/InvertibleIdealLocal.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponentSeshadri.UnitEndomorphism.unit line 12
  2. def OAI.PiExponentSeshadri.UnitEndomorphism.equation line 15
  3. lemma OAI.PiExponentSeshadri.UnitEndomorphism.app_eq_mul line 17
  4. lemma OAI.PiExponentSeshadri.UnitEndomorphism.image_principal line 23
  5. lemma OAI.PiExponentSeshadri.UnitEndomorphism.equation_regular line 33
  6. lemma OAI.PiExponentSeshadri.InvertibleLocal.image_eq_comap line 51
  7. theorem OAI.PiExponentSeshadri.InvertibleLocal.mono_comp_iso line 59
  8. theorem OAI.PiExponentSeshadri.InvertibleLocal.mono_iso_inv_comp line 62

    Also declared: OAI/NumberTheory/PiExponent/LocalAlgebra/GlobalInvertibleIdeal.lean:39 (same declaration text).

  9. def OAI.PiExponentSeshadri.InvertibleLocal.restrictedInclusion line 65
  10. instance OAI.PiExponentSeshadri.InvertibleLocal.restrictedInclusion_mono line 69
  11. lemma OAI.PiExponentSeshadri.InvertibleLocal.restricted_image line 74
  12. lemma OAI.PiExponentSeshadri.InvertibleLocal.local_equation line 98
  13. lemma OAI.PiExponentSeshadri.InvertibleLocal.affine_local_equation line 130
  14. def OAI.PiExponentSeshadri.InvertibleLocal.restrictLineBundle line 147
  15. lemma OAI.PiExponentSeshadri.InvertibleLocal.presents_restrict line 161
  16. lemma OAI.PiExponentSeshadri.InvertibleLocal.invertible_restrict line 172