Theorem Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton

Modification history

2026-02-09 11:07
Mathlib/RingTheory/Ideal/GoingUp.lean
feat(RingTheory): local structure for finite unramified algebras (#34928)
Added Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singletonView on Github →