OAI/NumberTheory/PiExponent/LocalAlgebra/IdealPowerAnnihilator.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponentSeshadri.IdealModule.hom_ext_affine line 12
  2. lemma OAI.PiExponentSeshadri.IdealModule.restriction_mem_ideal line 23
  3. lemma OAI.PiExponentSeshadri.IdealModule.smul_closedInclusion_structureMap_eq_zero line 34
  4. def OAI.PiExponentSeshadri.IdealModule.multiplyToNextPower line 52
  5. lemma OAI.PiExponentSeshadri.IdealModule.multiplyToNextPower_inclusion line 58
  6. lemma OAI.PiExponentSeshadri.IdealModule.multiplyToNextPower_powerMap line 63
  7. theorem OAI.PiExponentSeshadri.IdealModule.powerLayer_smul_id_eq_zero line 75