Commit 2026-02-07 14:43 e8bd29a9

View on Github →

chore(RingTheory): split QuasiFinite/Basic.lean (#34946)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/QuasiFinite/Basic.lean

deleted theorem Polynomial.map_under_lt_comap_of_quasiFiniteAt

deleted theorem Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt

deleted theorem Polynomial.not_quasiFiniteAt

Created Mathlib/RingTheory/QuasiFinite/Polynomial.lean

added theorem Polynomial.map_under_lt_comap_of_quasiFiniteAt

added theorem Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt

added theorem Polynomial.not_quasiFiniteAt