Commit 2026-01-22 12:40 a65eb1ae

View on Github →

feat(RingTheory): predicate for QuasiFiniteAt (#33718)

Estimated changes

Modified Mathlib/Algebra/Module/FinitePresentation.lean

added theorem IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation

Modified Mathlib/RingTheory/Etale/QuasiFinite.lean

deleted theorem Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver

Modified Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

added theorem RingHom.SurjectiveOnStalks.residueFieldMap_bijective

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

deleted theorem IsLocalization.AtPrime.liesOver_maximalIdeal

Modified Mathlib/RingTheory/QuasiFinite/Basic.lean

added theorem Algebra.QuasiFiniteAt.baseChange

added theorem Algebra.QuasiFiniteAt.eq_of_le_of_under_eq

added theorem Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton

added theorem Algebra.QuasiFiniteAt.isClopen_singleton

added theorem Algebra.QuasiFiniteAt.of_le

added theorem Algebra.QuasiFiniteAt.of_surjectiveOnStalks

added theorem Algebra.QuasiFiniteAt.of_surjectiveOnStalks_of_liesOver

added theorem Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver

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