Commit 2025-12-20 21:16 c5f79a7f

View on Github →

feat(RingTheory/FinitePresentation): a finite product of finitely presented algebras is finitely presented (#32758) From Pi1.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Pi.lean

modified theorem Pi.mulSingle_induction

modified theorem Pi.single_induction

Modified Mathlib/RingTheory/Ideal/Basic.lean

added theorem Ideal.span_single_eq_top

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem RingHom.ker_evalRingHom

Modified Mathlib/RingTheory/RingHom/FinitePresentation.lean

added theorem Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway