All.lean
Nyll.SchemeTheory.RingTheory.Flat.All
0 declarations indexed from sourceView source ↗
Module documentation
Flatness criteria and finite models
This aggregate exposes local flatness criteria, generic flatness, openness of the flat locus, and finite-subalgebra models.
Imports8
- Nyll.SchemeTheory.RingTheory.Flat.LocalCriterion
- Nyll.SchemeTheory.RingTheory.Flat.GenericFlatness
- Nyll.SchemeTheory.RingTheory.Flat.OpenLocus
- Nyll.SchemeTheory.RingTheory.Flat.FiniteSubalgebraLocalization
- Nyll.SchemeTheory.RingTheory.Flat.FiniteSubalgebra
- Nyll.SchemeTheory.RingTheory.Flat.Kernel
- Nyll.SchemeTheory.RingTheory.Flat.TensorInjectivity
- Nyll.SchemeTheory.RingTheory.Flat.TensorExactness
Imported by1
This module has no indexed declarations. Its imports and full source are available here.