All.lean
Nyll.AlgebraicCurves.Divisors.Semilinear.All
0 declarations indexed from sourceView source ↗
Imports17
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_correspondence_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_eq_of_baseAut_eq_of_forall_smul_place_eq
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_eq_of_forall_smul_place_eq
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_existsUnique_monoidHom_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_exists_baseAut_eq_of_constantFieldExtension
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_inertiaDeg_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_ofAlgAut_smul_place
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_ord_algebraMap_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pic0_correspondence_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pic0_correspondence_swap_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pullbackAlong_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pullback_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pushforwardAlong_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pushforward_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_ramificationIndex_smul
- Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_restrict_smul
Imported by1
This module has no indexed declarations. Its imports and full source are available here.