OAI/NumberTheory/PiExponent/LocalAlgebra/IdealPowerRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.IdealModule.closedQuotientRestrictIso line 11
  2. def OAI.PiExponentSeshadri.IdealModule.closedQuotientCongr line 19
  3. def OAI.PiExponentSeshadri.IdealModule.powerLayerRestrictIso line 25
  4. theorem OAI.PiExponentSeshadri.IdealModule.powerLayer_restrict_smul_eq_zero line 31
  5. theorem OAI.PiExponentSeshadri.IdealModule.ker_subscheme_morphismRestrict line 46
  6. theorem OAI.PiExponentSeshadri.IdealModule.ker_appTop_subscheme_morphismRestrict line 55
  7. theorem OAI.PiExponentSeshadri.IdealModule.powerLayer_restrict_kernel_smul_eq_zero line 64