All.lean
Nyll.AlgebraicCurves.Geometry.All
0 declarations indexed from sourceView source ↗
Imports27
- Nyll.AlgebraicCurves.Geometry.AbelianSchemes.All
- Nyll.AlgebraicCurves.Geometry.Curves.All
- Nyll.AlgebraicCurves.Geometry.Deformation.All
- Nyll.AlgebraicCurves.Geometry.Descent.All
- Nyll.AlgebraicCurves.Geometry.Picard.All
- Nyll.AlgebraicCurves.Geometry.Projective.All
- Nyll.AlgebraicCurves.Geometry.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
- Nyll.AlgebraicCurves.Geometry.Exists_D_ne_zero
- Nyll.AlgebraicCurves.Geometry.Exists_bounded_two_cochain_of_local_coboundaries
- Nyll.AlgebraicCurves.Geometry.Exists_coboundary_at_infinity_of_smallExtension_of_split
- Nyll.AlgebraicCurves.Geometry.Exists_disc_sections_locality_of_henselSections_of_weierstrassPreparation
- Nyll.AlgebraicCurves.Geometry.Exists_injective_ell_sub_sum_single_eq_zero_of_card_le
- Nyll.AlgebraicCurves.Geometry.Exists_int_forall_degree_add_one_sub_le_ell
- Nyll.AlgebraicCurves.Geometry.Exists_isRational_forall_mem_and_evalAt_eq_of_algHom
- Nyll.AlgebraicCurves.Geometry.Exists_local_coboundary_of_smallExtension_of_monogenic_fibre
- Nyll.AlgebraicCurves.Geometry.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
- Nyll.AlgebraicCurves.Geometry.FundamentalIdentityAlong
- Nyll.AlgebraicCurves.Geometry.Inv_smul_D_eq_zero_iff_exists_pow_eq
- Nyll.AlgebraicCurves.Geometry.IsClosed_singleton_of_ne_genericPoint
- Nyll.AlgebraicCurves.Geometry.Map_ne_zero_of_tame
- Nyll.AlgebraicCurves.Geometry.Mem_of_mul_eval2_mem_of_forall_coeff_mem_maximalIdeal
- Nyll.AlgebraicCurves.Geometry.Nonempty_algEquiv_functionField_of_iso
- Nyll.AlgebraicCurves.Geometry.One_le_deg
- Nyll.AlgebraicCurves.Geometry.WeilReciprocity
- Nyll.AlgebraicCurves.Geometry.WeilReciprocity_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Schemes.All
- Nyll.AlgebraicCurves.Geometry.Sheaves.All
Imported by1
This module has no indexed declarations. Its imports and full source are available here.