All.lean
Nyll.SchemeTheory.FunctionFields.PrimeDivisors.All
0 declarations indexed from sourceView source ↗
Module documentation
Prime divisors of function fields
This aggregate exposes centered prime divisors, degree and counting comparisons, integral-closure primes, divisors at infinity, and transport across function-field maps.
Imports11
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Basic
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Centered
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.CenteredTransport
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Counting
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Dedekind
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.DegreeOne
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Infinity
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.InseparableCounting
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.IntegralClosure
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.PrimesOver
- Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Transport
Imported by1
This module has no indexed declarations. Its imports and full source are available here.