Commit 2024-02-01 18:09 6dd08a56

View on Github →

feat(RingTheory/Flat): definition of flat ring homomorphism and stability under composition (#10148) Adds the definition of flat algebras, flat ring homomorphisms and shows that flatness is stable under composition.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added def TensorProduct.AlgebraTensorModule.cancelBaseChange

added theorem TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul

added theorem TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul

Created Mathlib/RingTheory/Flat/Algebra.lean

added theorem Algebra.Flat.comp

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem Module.Flat.iff_lTensor_injective'

added theorem Module.Flat.iff_lTensor_injective

added theorem Module.Flat.lTensor_inj_iff_rTensor_inj

Created Mathlib/RingTheory/Flat/Stability.lean

added theorem Module.Flat.comp