Theorem Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective

Modification history

2026-02-09 11:07
Mathlib/RingTheory/Unramified/LocalStructure.lean
feat(RingTheory): local structure for finite unramified algebras (#34928)
Added Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijectiveView on Github →