Theorem Module.Finite.of_finite_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 Module.Finite.of_finite_tensorProduct_of_faithfullyFlatView on Github →