All.lean
Nyll.AlgebraicCurves.FunctionFields.All
0 declarations indexed from sourceView source ↗
Imports84
- Nyll.AlgebraicCurves.FunctionFields.CurveOver
- Nyll.AlgebraicCurves.FunctionFields.Kummer.All
- Nyll.AlgebraicCurves.FunctionFields.LaurentBaseChange
- Nyll.AlgebraicCurves.FunctionFields.Cartier_map_eq_map_cartier_of_constantFieldExtension
- Nyll.AlgebraicCurves.FunctionFields.CompletionTraceSum_of_isSeparable
- Nyll.AlgebraicCurves.FunctionFields.ConstantFieldDegreeFormula_of_isConstantFieldExtension_of_isCurveOver
- Nyll.AlgebraicCurves.FunctionFields.ConstantsAreBase_of_deg_eq_one
- Nyll.AlgebraicCurves.FunctionFields.ConstantsAreBase_of_exists_isRational
- Nyll.AlgebraicCurves.FunctionFields.ConstantsAreBase_of_isAlgClosed
- Nyll.AlgebraicCurves.FunctionFields.ConstantsAreBase_of_isAlgClosed_of_transcendental
- Nyll.AlgebraicCurves.FunctionFields.Discr_ne_zero_of_normalForm_split
- Nyll.AlgebraicCurves.FunctionFields.EssFiniteType_functionField
- Nyll.AlgebraicCurves.FunctionFields.EssFiniteType_of_transcendental_of_finiteDimensional
- Nyll.AlgebraicCurves.FunctionFields.Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed
- Nyll.AlgebraicCurves.FunctionFields.Exists_algEquiv_comp_eq_of_ker_eq_of_closure_range_eq_top_of_finrankAlong_eq
- Nyll.AlgebraicCurves.FunctionFields.Exists_centre_and_finite_setOf_centre_of_isClosed_singleton
- Nyll.AlgebraicCurves.FunctionFields.Exists_constantFieldDescent
- Nyll.AlgebraicCurves.FunctionFields.Exists_constantFieldDescent_finset
- Nyll.AlgebraicCurves.FunctionFields.Exists_constantFieldExtension
- Nyll.AlgebraicCurves.FunctionFields.Exists_constantFieldExtension_of_finite
- Nyll.AlgebraicCurves.FunctionFields.Exists_derivation_constantFieldExtension_map_mem
- Nyll.AlgebraicCurves.FunctionFields.Exists_ell_nsmul_eq_of_isAlgClosed_of_transcendental
- Nyll.AlgebraicCurves.FunctionFields.Exists_finiteDimensional_isSeparable_adjoin_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.FunctionFields.Exists_finiteDimensional_isSeparable_adjoin_of_constantFieldExtension_of_perfectField
- Nyll.AlgebraicCurves.FunctionFields.Exists_isCurveOver_adjoin_range_eq_top_apply_algEquiv_eq_pow_of_pow_eq_one
- Nyll.AlgebraicCurves.FunctionFields.Exists_lift_normalForm_structureConstants_of_smallExtension
- Nyll.AlgebraicCurves.FunctionFields.Exists_mem_D_eq_smul_D_of_isCurveOver
- Nyll.AlgebraicCurves.FunctionFields.Exists_separating_transcendental_of_perfectField
- Nyll.AlgebraicCurves.FunctionFields.Exists_wittVector_lift_of_normalFormOrder
- Nyll.AlgebraicCurves.FunctionFields.FiniteAlong_comp
- Nyll.AlgebraicCurves.FunctionFields.FiniteAlong_of_isIntegral
- Nyll.AlgebraicCurves.FunctionFields.FiniteAlong_of_surjective
- Nyll.AlgebraicCurves.FunctionFields.FiniteDimensional_adjoin_of_transcendental
- Nyll.AlgebraicCurves.FunctionFields.Finite_and_card_torsion_le_pow_finrank
- Nyll.AlgebraicCurves.FunctionFields.Finite_intermediateField_of_transcendental_mem
- Nyll.AlgebraicCurves.FunctionFields.FinrankAlong_comp
- Nyll.AlgebraicCurves.FunctionFields.FinrankAlong_eq_and_trace_eq_of_constantFieldExtension
- Nyll.AlgebraicCurves.FunctionFields.FinrankAlong_eq_and_trace_eq_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.FunctionFields.FinrankAlong_eq_relfinrank_fieldRange
- Nyll.AlgebraicCurves.FunctionFields.FinrankAlong_id
- Nyll.AlgebraicCurves.FunctionFields.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
- Nyll.AlgebraicCurves.FunctionFields.FunctionField_exists_ratFuncAlgHom_apply_X_eq
- Nyll.AlgebraicCurves.FunctionFields.FunctionField_finite_of_ratFuncAlgHom
- Nyll.AlgebraicCurves.FunctionFields.Infinite_setOf_isClosed_singleton
- Nyll.AlgebraicCurves.FunctionFields.InstIsCurveOverRatFunc
- Nyll.AlgebraicCurves.FunctionFields.IsAlgebraic_adjoin_of_transcendental
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_and_essFiniteType_and_exists_of_adjoin_finset_eq_top_of_isAlgebraic
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_and_essFiniteType_intermediateField_of_transcendental_mem
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_and_essFiniteType_of_le_of_transcendental_mem
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_exists_separating_transcendental
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_finiteDimensional_adjoin_simple_of_transcendental_of_essFiniteType
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_iff_exists_transcendental_finiteDimensional
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_of_isAlgClosed_of_transcendental
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_of_transcendental
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_of_transcendental_of_isSeparable
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_of_transcendental_of_perfectField
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_ratFunc
- Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_trdeg_eq_one
- Nyll.AlgebraicCurves.FunctionFields.IsIntegral_adjoin_intermediateField_mk
- Nyll.AlgebraicCurves.FunctionFields.IsIntegral_adjoin_map_algHom
- Nyll.AlgebraicCurves.FunctionFields.IsIntegral_adjoin_of_isScalarTower
- Nyll.AlgebraicCurves.FunctionFields.IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.FunctionFields.LinearIndependent_algebraMap_of_constantsAreBase_of_isAlgebraic
- Nyll.AlgebraicCurves.FunctionFields.LinearIndependent_of_constantFieldExtension
- Nyll.AlgebraicCurves.FunctionFields.LinearIndependent_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.FunctionFields.LinearIndependent_pow_mul
- Nyll.AlgebraicCurves.FunctionFields.LinearIndependent_pow_mul_of_flagAdaptedBasisAt_of_ell_eq
- Nyll.AlgebraicCurves.FunctionFields.LinearIndependent_pow_of_transcendental
- Nyll.AlgebraicCurves.FunctionFields.Mem_range_algebraMap_of_isAlgebraic
- Nyll.AlgebraicCurves.FunctionFields.Mem_span_range_algebraMap_of_constantFieldExtension
- Nyll.AlgebraicCurves.FunctionFields.Mem_span_range_algebraMap_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.FunctionFields.RelNorm_eq_pow_of_isMaximal_of_isSeparable
- Nyll.AlgebraicCurves.FunctionFields.SeparableAlong_of_charZero
- Nyll.AlgebraicCurves.FunctionFields.Surjective_and_ker_pi_span_mul_quotient_of_finite
- Nyll.AlgebraicCurves.FunctionFields.TraceIntegralAlong_of_separableAlong
- Nyll.AlgebraicCurves.FunctionFields.TranscendenceTower_degree_poleDivisor_eq_finrank
- Nyll.AlgebraicCurves.FunctionFields.TranscendenceTower_poleDivisor_apply
- Nyll.AlgebraicCurves.FunctionFields.WeilReciprocity_algebraMap
- Nyll.AlgebraicCurves.FunctionFields.WeilReciprocity_algebraMap_of_isSeparable
- Nyll.AlgebraicCurves.FunctionFields.NormSurjectiveOfTsen
- Nyll.AlgebraicCurves.FunctionFields.CyclicH2OfTsen
- Nyll.AlgebraicCurves.FunctionFields.PGroupH2OfTsen
- Nyll.AlgebraicCurves.FunctionFields.GaloisH2OfTsen
- Nyll.AlgebraicCurves.FunctionFields.AbsoluteModPTwoCocycleOfTsen
Imported by1
This module has no indexed declarations. Its imports and full source are available here.