DivisorialPointedQuotientEveryPrime.lean

Divisorial inertia detected at every prime

Coprimality of one actual pointed finite inertia image with every rational prime forces the corresponding normalization-prime ideal inertia subgroup to be trivial.

The declaration is implemented in DivisorialPointedQuotientEndpoint, beside the comparison theorem whose local instance graph it reuses. This module is the narrow compatibility facade.