Theorem PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply

Modification history

2026-06-04 10:17
Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean
feat(RingTheory/RamificationInertia/Ramification): positivity of ramification index (#39977) …
Added PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_applyView on Github →