Theorem Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway

Modification history

2026-03-03 14:56

Mathlib/RingTheory/Finiteness/FinitePresentationLocal.lean

chore(RingTheory): reorganize imports around locality properties of finiteness (#36044)

Modified Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway View on Github →

2025-12-20 21:16

Mathlib/RingTheory/RingHom/FinitePresentation.lean

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

Added Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway View on Github →