Theorem Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt

Modification history

2026-02-13 17:17
Mathlib/RingTheory/QuasiFinite/Polynomial.lean
feat(RingTheory): weakly quasi finite primes (#35234)
Added Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAtView on Github →