Theorem Polynomial.map_under_lt_comap_of_quasiFiniteAt

Modification history

2026-02-07 14:43
Mathlib/RingTheory/QuasiFinite/Basic.lean
chore(RingTheory): split `QuasiFinite/Basic.lean` (#34946)
Modified Polynomial.map_under_lt_comap_of_quasiFiniteAtView on Github →
2026-01-22 12:40
Mathlib/RingTheory/QuasiFinite/Basic.lean
feat(RingTheory): predicate for `QuasiFiniteAt` (#33718)
Added Polynomial.map_under_lt_comap_of_quasiFiniteAtView on Github →