Theorem Algebra.TensorProduct.map_surjective

Modification history

2026-02-13 17:17
Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
feat(RingTheory): weakly quasi finite primes (#35234)
Added Algebra.TensorProduct.map_surjectiveView on Github →