OAI/AlgebraicGeometry/Seshadri/Divisors/IdealSectionLifting.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Geometry.pullback_affine_coefficient line 19
2. lemma OAI.MaximalSeshadri.Geometry.InvertibleLocal.pullback_frame_equation line 36
3. lemma OAI.MaximalSeshadri.Geometry.ideal_power_tensor_equation line 70
4. theorem OAI.MaximalSeshadri.Geometry.lift_section_of_local_ideal_power line 86