Commit 2024-12-09 08:25 8f0293e9
View on Github →chore(RingTheory/Flat): remove Algebra.Flat and move RingHom.Flat (#19786)
We remove Algebra.Flat as it is a special case of Module.Flat and make RingHom.Flat a regular definition to align with e.g. RingHom.Finite. Also adds some meta properties of flat ring homomorphisms.