All.lean
Nyll.AlgebraicCurves.Differentials.All
0 declarations indexed from sourceView source ↗
Imports63
- Nyll.AlgebraicCurves.Differentials.Basic
- Nyll.AlgebraicCurves.Differentials.Cartier.All
- Nyll.AlgebraicCurves.Differentials.CartierCoordinates
- Nyll.AlgebraicCurves.Differentials.CartierFixedness
- Nyll.AlgebraicCurves.Differentials.Kaehler.All
- Nyll.AlgebraicCurves.Differentials.LocalCoordinate
- Nyll.AlgebraicCurves.Differentials.Logarithmic
- Nyll.AlgebraicCurves.Differentials.Maps
- Nyll.AlgebraicCurves.Differentials.Order
- Nyll.AlgebraicCurves.Differentials.Polar
- Nyll.AlgebraicCurves.Differentials.PthPowerKernel
- Nyll.AlgebraicCurves.Differentials.CartierOperator_existsUnique
- Nyll.AlgebraicCurves.Differentials.DCoordGenerates_of_isCurveOver
- Nyll.AlgebraicCurves.Differentials.Differential_correspondence_mem_regularDifferentials
- Nyll.AlgebraicCurves.Differentials.Differential_map_correspondence_eq_correspondence_map_of_separableAlong_of_constantFieldExtension
- Nyll.AlgebraicCurves.Differentials.Differential_map_correspondence_regularDifferentials_of_constantFieldExtension
- Nyll.AlgebraicCurves.Differentials.Differential_pullbackAlong_comp
- Nyll.AlgebraicCurves.Differentials.Differential_pullbackAlong_traceAlong_eq_sum_lifts
- Nyll.AlgebraicCurves.Differentials.Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv
- Nyll.AlgebraicCurves.Differentials.Differential_pullbackAlong_traceAlong_pullbackAlong_eq_traceAlong_pullbackAlong_pullbackAlong_of_swap
- Nyll.AlgebraicCurves.Differentials.Differential_sum_ord_smul_pullbackAlong_eq_zero
- Nyll.AlgebraicCurves.Differentials.Differential_traceAlong_eq_traceDiff
- Nyll.AlgebraicCurves.Differentials.Dlog_mem_regularDifferentials_of_forall_dvd_ord
- Nyll.AlgebraicCurves.Differentials.Dvd_ord_of_isRegularDiff_dlog
- Nyll.AlgebraicCurves.Differentials.Exists_dlog_of_cartierOperator_fixed
- Nyll.AlgebraicCurves.Differentials.Exists_isUnit_det_evalAt_differentialCoeff
- Nyll.AlgebraicCurves.Differentials.Exists_kaehlerToFunctionField_eq_smul_dCoord_of_mem_placesOf
- Nyll.AlgebraicCurves.Differentials.Exists_mem_smul_D_of_map_mem_regularDifferentials_of_constantFieldExtension
- Nyll.AlgebraicCurves.Differentials.Exists_ordDifferential_eq_neg_one_of_ne
- Nyll.AlgebraicCurves.Differentials.Exists_ordDifferential_ge_neg_one_and_evalAt_eq_of_degree_eq_zero
- Nyll.AlgebraicCurves.Differentials.Exists_smul_D_eq_smul_dCoord_of_forall_isIntegral_trace_mul_eq_aeval
- Nyll.AlgebraicCurves.Differentials.Exists_trace_mul_eq_aeval_of_forall_exists_smul_D_eq_smul_dCoord
- Nyll.AlgebraicCurves.Differentials.Exists_transcendental_isSeparable_of_finrank_kaehlerDifferential_eq_one
- Nyll.AlgebraicCurves.Differentials.Finite_and_finrank_polarDifferentials_eq
- Nyll.AlgebraicCurves.Differentials.IsRegularDiff_dlog_of_dvd_ord
- Nyll.AlgebraicCurves.Differentials.IsTraceDiff_traceDiff
- Nyll.AlgebraicCurves.Differentials.KaehlerDifferential_map_injective_of_constantFieldExtension
- Nyll.AlgebraicCurves.Differentials.KaehlerRankOne_of_transcendental
- Nyll.AlgebraicCurves.Differentials.Kw_cart_C_eq_of_cartierLaws
- Nyll.AlgebraicCurves.Differentials.Kw_cart_C_pow_pred_smul_D
- Nyll.AlgebraicCurves.Differentials.Kw_cart_C_pow_smul_D_eq_zero
- Nyll.AlgebraicCurves.Differentials.LocalUnitDerivativeRegular_of_isCurveOver
- Nyll.AlgebraicCurves.Differentials.Map_mem_polarDifferentials_and_mem_span_image_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Differentials.Map_mem_polarDifferentials_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Differentials.Mem_regularDiffs_iff
- Nyll.AlgebraicCurves.Differentials.Mem_span_image_polarDifferentials_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Differentials.OrdDifferential_map_eq
- Nyll.AlgebraicCurves.Differentials.PullbackAlong_mem_regularDifferentials_of_isIntegral
- Nyll.AlgebraicCurves.Differentials.PullbackAlong_mem_regularDifferentials_of_mem_of_algEquiv
- Nyll.AlgebraicCurves.Differentials.PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver
- Nyll.AlgebraicCurves.Differentials.PullbackDiff_smul
- Nyll.AlgebraicCurves.Differentials.RegularDiffs_eq_regularDifferentials
- Nyll.AlgebraicCurves.Differentials.RegularDiffs_eq_regularDifferentials_of_perfectField
- Nyll.AlgebraicCurves.Differentials.Sum_fibre_evalAt_eq_zero_of_smul_D_mem_regularDifferentials
- Nyll.AlgebraicCurves.Differentials.TraceDiff_apply
- Nyll.AlgebraicCurves.Differentials.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm
- Nyll.AlgebraicCurves.Differentials.Twelve_mul_eq_of_sum_ordDiff_eq
- Nyll.AlgebraicCurves.Differentials.WeilDifferentialRankOne_of_isCurveOver
- Nyll.AlgebraicCurves.Differentials.WeilOfKaehler_ne_zero_and_maximal
- Nyll.AlgebraicCurves.Differentials.Regular
- Nyll.AlgebraicCurves.Differentials.Residues.All
- Nyll.AlgebraicCurves.Differentials.Trace
- Nyll.AlgebraicCurves.Differentials.Uniformizer
Imported by1
This module has no indexed declarations. Its imports and full source are available here.