Theorem TensorProduct.mk_surjective

Modification history

2024-07-05 09:16
Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
feat(RingTheory/LocalRing/Module): Finitely presented flat modules over local rings are free. (#14375)
Added TensorProduct.mk_surjectiveView on Github →