Commit 2025-01-02 11:03 758574f8

View on Github →

feat(Algebra): auxiliary lemmas for flatness over semirings (#20265)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Module.lean

added def DirectSum.lmap

added theorem DirectSum.lmap_apply

added theorem DirectSum.lmap_injective

added theorem DirectSum.lmap_lof

Modified Mathlib/Algebra/Module/Injective.lean

added theorem Module.Baer.congr

added theorem Module.Baer.of_equiv

Modified Mathlib/Data/DFinsupp/Defs.lean

added theorem DFinsupp.mapRange_injective

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

added theorem TensorProduct.directSumRight_comp_rTensor

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange

Modified Mathlib/RingTheory/Finiteness/Cardinality.lean

added theorem Module.Finite.small

Modified Mathlib/RingTheory/Finiteness/TensorProduct.lean

modified theorem Submodule.exists_fg_le_eq_rTensor_inclusion

added theorem Submodule.exists_fg_le_eq_rTensor_subtype

added theorem Submodule.exists_fg_le_subset_range_rTensor_inclusion

added theorem Submodule.exists_fg_le_subset_range_rTensor_subtype

Modified Mathlib/RingTheory/Flat/CategoryTheory.lean

Modified Mathlib/RingTheory/Localization/BaseChange.lean