Theorem RingHom.surjective_of_tmul_eq_tmul_of_finite

Modification history

2026-01-15 19:06
Mathlib/RingTheory/TensorProduct/Finite.lean
feat: the rank of the ℤ-span of the roots of a root system is the dimension (#33846) …
Deleted RingHom.surjective_of_tmul_eq_tmul_of_finiteView on Github →
2024-11-06 15:34
Mathlib/RingTheory/TensorProduct/Finite.lean
feat(Algebra/Category): for ring homs, epi + finite => surjective (#18267)
Added RingHom.surjective_of_tmul_eq_tmul_of_finiteView on Github →