All.lean
Nyll.AlgebraicCurves.Places.Rational.All
0 declarations indexed from sourceView source ↗
Imports44
- Nyll.AlgebraicCurves.Places.Rational.Basic
- Nyll.AlgebraicCurves.Places.Rational.Classification
- Nyll.AlgebraicCurves.Places.Rational.Infinity
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_algebraMap_polynomial_mem_of_ne_placeInfty
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_deg_eq_one_of_forall_ne_ofHeightOneSpectrum
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_deg_eq_one_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_deg_ne_zero
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_deg_placeInfty
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_degree_eq_zero_of_forall_eq_ord
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_degree_eq_zero_of_isPrincipal
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ell_sub_ell_eq_genus_zero
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_eq_placeInfty_iff_forall_ne_ofHeightOneSpectrum
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_eq_placeInfty_of_ord_X_neg
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_evalAt_placeInfty_eq
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_evalAt_placeOfPoint_algebraMap
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_exists_algEquiv_congrRingEquiv_placeInfty_eq_placeOfPoint_zero_eq
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_finiteDimensional_lSpace_zero_of_constantsAreBase
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_finite_setOf_ord_ne_zero
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_hasPrincipalDivisors
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_indexOfSpecialtyFinite_of_ratFunc_tower
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_isPrincipal_of_degree_eq_zero
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_mapDomain_eq_ord_div_map_of_primitive
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_nonempty_place_of_ratFunc_tower
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_X_nonneg_of_ne_placeInfty
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_X_sub_C
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_eq_neg_intDegree_of_forall_ne_ofHeightOneSpectrum
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_ofHeightOneSpectrum_eq_neg_log
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_ofHeightOneSpectrum_of_span
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_placeInfty
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_placeInfty_X
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_placeInfty_algebraMap
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_placeInfty_eq_ord_placeInfty_add_sum_ord_placeOfPoint_of_reduction
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_placeOfPoint_algebraMap
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_stichtenothGenusExists
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_stichtenothGenusExists_of_ratFunc_tower
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_subsingleton_setOf_forall_ne_ofHeightOneSpectrum
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_toValuationSubring_eq_of_forall_ne_ofHeightOneSpectrum
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_trace_localResidue_finitePlace_add_trace_localResidue_placeInfty_eq_zero
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_trace_localResidue_finitePlace_div_pow_eq_zero
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_trace_localResidue_placeInfty_X_pow_eq_zero
- Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_weilReciprocity
Imported by1
This module has no indexed declarations. Its imports and full source are available here.