Commit 2026-02-13 17:17 0e4799ce

View on Github →

feat(RingTheory): weakly quasi finite primes (#35234)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

added theorem Algebra.TensorProduct.map_surjective

Modified Mathlib/RingTheory/QuasiFinite/Basic.lean

added theorem Algebra.QuasiFinite.iff_of_algEquiv

Modified Mathlib/RingTheory/QuasiFinite/Polynomial.lean

added theorem Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt

added theorem Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt

modified theorem Polynomial.not_quasiFiniteAt

added theorem Polynomial.not_weaklyQuasiFiniteAt

Created Mathlib/RingTheory/QuasiFinite/Weakly.lean

added theorem Algebra.WeaklyQuasiFiniteAt.baseChange

added theorem Algebra.WeaklyQuasiFiniteAt.eq_of_le_of_under_eq

added theorem Algebra.WeaklyQuasiFiniteAt.finite_locoalization

added theorem Algebra.WeaklyQuasiFiniteAt.finite_residueField

added theorem Algebra.WeaklyQuasiFiniteAt.of_algHom_localization

added theorem Algebra.WeaklyQuasiFiniteAt.of_restrictScalars

added theorem Algebra.WeaklyQuasiFiniteAt.of_surjectiveOnStalks

added theorem Algebra.weaklyQuasiFiniteAt_iff

Modified Mathlib/RingTheory/SurjectiveOnStalks.lean

added theorem RingHom.SurjectiveOnStalks.localRingHom_surjective

Modified Mathlib/RingTheory/ZariskisMainTheorem.lean

added theorem Algebra.QuasiFiniteAt.of_weaklyQuasiFiniteAt

added theorem Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt.{u,

added theorem Algebra.ZariskisMainProperty.quasiFiniteAt