All.lean
Nyll.AlgebraicCurves.Foundations.FieldTheory.All
0 declarations indexed from sourceView source ↗
Imports17
- Nyll.AlgebraicCurves.Foundations.FieldTheory.FrobeniusSubfield
- Nyll.AlgebraicCurves.Foundations.FieldTheory.Mathlib_FieldTheory_RatFuncImperfectionDegree
- Nyll.AlgebraicCurves.Foundations.FieldTheory.AdjoinRoot_etale_and_finite_X_pow_sub_C_of_isUnit
- Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_IsSeparable_of_finrank_fieldRange_frobenius_eq
- Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_TensorProduct_isField_of_isSeparable_of_forall_isAlgebraic_mem_range
- Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range
- Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_TensorProduct_nilradical_isPrime_of_isAlgebraic_of_forall_isSeparable_mem_range
- Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_exists_algHom_forall_apply_ne_zero_of_finiteType_of_isAlgClosed
- Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_exists_monic_irreducible_map_algebraicClosure_hypersurfaceModel_of_forall_isSeparable
- Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
- Nyll.AlgebraicCurves.Foundations.FieldTheory.IntermediateField_finiteDimensional_adjoin_of_linearDisjoint_of_transcendental
- Nyll.AlgebraicCurves.Foundations.FieldTheory.IntermediateField_finrank_adjoin_range_le_finrank_of_transcendental
- Nyll.AlgebraicCurves.Foundations.FieldTheory.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
- Nyll.AlgebraicCurves.Foundations.FieldTheory.IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
- Nyll.AlgebraicCurves.Foundations.FieldTheory.IsSeparable_of_algHom_apply_eq_pow_of_transcendental
- Nyll.AlgebraicCurves.Foundations.FieldTheory.Module_Flat_mem_nonZeroDivisors_and_flat_quotient_span_of_forall_isAlgClosed
- Nyll.AlgebraicCurves.Foundations.FieldTheory.TensorFractionGeneration
Imported by1
This module has no indexed declarations. Its imports and full source are available here.