Theorem Ideal.FG.of_FG_map_of_faithfullyFlat

Modification history

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