All.lean
Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Compositum.All
0 declarations indexed from sourceView source ↗
Module documentation
Valued composita for the tame Abhyankar frontier
This module is an umbrella for the valued-compositum layer. The implementation uses the shared record-free compositum facts and the canonical common-top square arguments. The former one-sided wrapper layers duplicated these consequences and have been removed.
Imports3
This module has no indexed declarations. Its imports and full source are available here.