Theorem RingHom.Finite.codescendsAlong_faithfullyFlat

Modification history

2026-02-13 16:00
Mathlib/RingTheory/Finiteness/Descent.lean
feat(RingTheory): `Algebra.FinitePresentation` descends along faithfully flat algebras (#35254) …
Added RingHom.Finite.codescendsAlong_faithfullyFlatView on Github →