OAI/AlgebraicGeometry/Seshadri/LocalAlgebra/TwistedIdealPower.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Geometry.twistIdealPowerIso line 18
2. def OAI.MaximalSeshadri.Geometry.twistedIdealPowerInclusion line 25
3. lemma OAI.MaximalSeshadri.Geometry.twistedIdealPowerInclusion_mono line 30
4. def OAI.MaximalSeshadri.Geometry.twistedIdealPowerFrame line 37
5. lemma OAI.MaximalSeshadri.Geometry.affineMapCoefficient_iso_left line 44
6. lemma OAI.MaximalSeshadri.Geometry.twistedIdealPowerInclusion_ideal line 52