Theorem Ideal.exists_mem_span_singleton_map_residueField_eq

Modification history

2026-02-06 15:35
Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean
feat(RingTheory): local structure of monogenic unramified algebras (#33903)
Added Ideal.exists_mem_span_singleton_map_residueField_eqView on Github →