Commit 2024-07-05 09:16 46dd6dad

View on Github →

feat(RingTheory/LocalRing/Module): Finitely presented flat modules over local rings are free. (#14375)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

added theorem TensorProduct.mk_surjective

Created Mathlib/RingTheory/LocalRing/Module.lean

added theorem LocalRing.map_mkQ_eq

added theorem LocalRing.map_mkQ_eq_top

added theorem LocalRing.map_tensorProduct_mk_eq_top

added theorem LocalRing.span_eq_top_of_tmul_eq_basis

added theorem LocalRing.split_injective_iff_lTensor_residueField_injective

added theorem LocalRing.subsingleton_tensorProduct

added theorem Module.free_of_flat_of_localRing

added theorem Module.free_of_lTensor_residueField_injective

added theorem Module.free_of_maximalIdeal_rTensor_injective

added theorem lTensor_injective_of_exact_of_exact_of_rTensor_injective