Theorem Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt

Modification history

2026-01-22 12:40
Mathlib/RingTheory/QuasiFinite/Basic.lean
feat(RingTheory): predicate for `QuasiFiniteAt` (#33718)
Added Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAtView on Github →