All.lean
Nyll.JacobianVarieties.Pic0.All
0 declarations indexed from sourceView source ↗
Imports43
- Nyll.JacobianVarieties.Pic0.PullbackAlong
- Nyll.JacobianVarieties.Pic0.PushforwardAlong
- Nyll.JacobianVarieties.Pic0.BaseChange
- Nyll.AlgebraicCurves.Divisors.Pic0Congr
- Nyll.JacobianVarieties.Pic0.GenusFF_eq_and_nonempty_pic0_addEquiv_of_algebraMap_eq_comp
- Nyll.JacobianVarieties.Pic0.Pic0_addOrderOf_mk_dvd_of_isPrincipal
- Nyll.JacobianVarieties.Pic0.Pic0_conorm_correspondence_eq_correspondence_conorm
- Nyll.JacobianVarieties.Pic0.Pic0_conorm_smul_eq_smul_conorm_of_semilinearAut_compatible
- Nyll.JacobianVarieties.Pic0.Pic0_correspondence_correspondence_comm
- Nyll.JacobianVarieties.Pic0.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
- Nyll.JacobianVarieties.Pic0.Pic0_exists_equiv_points_add_and_poincare_iso_ofPoint_of_representsRelSubPic_of_curveModel
- Nyll.JacobianVarieties.Pic0.Pic0_exists_equiv_points_add_and_poincare_iso_ofPoint_of_representsRelSubPic_of_curveModel_of_isAlgClosed
- Nyll.JacobianVarieties.Pic0.Pic0_exists_injective_addMonoidHom_torsion_apply_eq_inv_smul_D
- Nyll.JacobianVarieties.Pic0.Pic0_exists_injective_addMonoidHom_torsion_dlog
- Nyll.JacobianVarieties.Pic0.Pic0_exists_injective_conorm_of_constantFieldExtension_of_isAlgClosed
- Nyll.JacobianVarieties.Pic0.Pic0_exists_jacobianPack_of_isAlgClosed
- Nyll.JacobianVarieties.Pic0.Pic0_exists_mk_eq_and_dvd_ord_of_mem_torsion
- Nyll.JacobianVarieties.Pic0.Pic0_exists_mk_eq_forall_notMem_support
- Nyll.JacobianVarieties.Pic0.Pic0_exists_nsmul_eq_of_jacobianPack_of_natCast_ne_zero
- Nyll.JacobianVarieties.Pic0.Pic0_exists_ord_eq_mul_and_forall_pow_ne_of_ne_zero
- Nyll.JacobianVarieties.Pic0.Pic0_exists_ord_eq_mul_of_nsmul_mk_eq_zero
- Nyll.JacobianVarieties.Pic0.Pic0_exists_relativeGroupLaw_equiv_of_curveModel
- Nyll.JacobianVarieties.Pic0.Pic0_exists_schemeHomOver_pushforwardAlong_of_representsRelSubPic
- Nyll.JacobianVarieties.Pic0.Pic0_exists_zsmul_eq_of_finiteDimensional_ratFunc_of_forall_pow_eq_self
- Nyll.JacobianVarieties.Pic0.Pic0_forall_isPrincipal_of_ringEquiv
- Nyll.JacobianVarieties.Pic0.Pic0_mem_closure_mk_single_sub_single
- Nyll.JacobianVarieties.Pic0.Pic0_mem_closure_mk_single_sub_single_of_notMem
- Nyll.JacobianVarieties.Pic0.Pic0_mk_eq_zero_iff_exists_pow
- Nyll.JacobianVarieties.Pic0.Pic0_natCard_torsion_eq_of_constantFieldExtension
- Nyll.JacobianVarieties.Pic0.Pic0_nonempty_divisorialWeilPairingData
- Nyll.JacobianVarieties.Pic0.Pic0_nonempty_divisorialWeilPairingData_of_isAlgClosed
- Nyll.JacobianVarieties.Pic0.Pic0_nsmul_mk_eq_zero_of_isPrincipal
- Nyll.JacobianVarieties.Pic0.Pic0_pushforwardAlongHom_smul
- Nyll.JacobianVarieties.Pic0.Pic0_pushforwardHom_pullbackHom
- Nyll.JacobianVarieties.Pic0.Pic0_range_eq_setOf_cartier_fixed_and_isRegularDiff
- Nyll.JacobianVarieties.Pic0.Pic0_roof_package_of_surjective
- Nyll.JacobianVarieties.Pic0.Pic0_torsion_apply_eq_traceAlong_pullbackAlong_of_correspondence
- Nyll.JacobianVarieties.Pic0.Pic0_torsion_bijective_of_injective
- Nyll.JacobianVarieties.Pic0.Pic0_torsion_exists_addMonoidHom_eval_eq_pairing
- Nyll.JacobianVarieties.Pic0.Pic0_torsion_exists_forall_ord_eq_mul
- Nyll.JacobianVarieties.Pic0.Pic0_torsion_move_of_forall_isRational
- Nyll.JacobianVarieties.Pic0.Pic0_zsmul_mk_eq_zero_of_isPrincipal
- Nyll.JacobianVarieties.Pic0.RelativePic0DesignationBaseChange
Imported by1
This module has no indexed declarations. Its imports and full source are available here.