Theorem Algebra.FinitePresentation.of_finitePresentation_tensorProduct_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 Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlatView on Github →