All.lean
Nyll.AlgebraicCurves.Geometry.Descent.All
0 declarations indexed from sourceView source ↗
Imports11
- Nyll.AlgebraicCurves.Geometry.Descent.DescentAction
- Nyll.AlgebraicCurves.Geometry.Descent.FppfGmRepresentable
- Nyll.AlgebraicCurves.Geometry.Descent.DescentAction_effective_of_finiteEtale
- Nyll.AlgebraicCurves.Geometry.Descent.DescentAction_effective_of_finiteEtale_of_forall_orbit
- Nyll.AlgebraicCurves.Geometry.Descent.DescentAction_effective_of_isPullback_of_flat_surjective
- Nyll.AlgebraicCurves.Geometry.Descent.FaithfullyFlatProperties
- Nyll.AlgebraicCurves.Geometry.Descent.FiniteFaithfullyFlat
- Nyll.AlgebraicCurves.Geometry.Descent.GlobalRepresentation
- Nyll.AlgebraicCurves.Geometry.Descent.GroupGlobalRepresentation
- Nyll.AlgebraicCurves.Geometry.Descent.GroupOfMatching
- Nyll.AlgebraicCurves.Geometry.Descent.RepresentableMatching
Imported by1
This module has no indexed declarations. Its imports and full source are available here.