Linear.lean
Nyll.EtaleFundamentalGroups.Kummer.HigherRadical.LowerFactor.FixedIntegral.Linear
0 declarations indexed from sourceView source ↗
Module documentation
Higher-root linearity of the retained integral generic component
The linear generic-fibre comparison and its underlying ring equivalence share one construction in FixedIntegral.Basic. This module retains the established import path for the higher-root-linear comparison.
This module has no indexed declarations. Its imports and full source are available here.