Theorem Algebra.isEpi_iff_surjective_algebraMap_of_finite

Modification history

2026-01-15 19:06
Mathlib/Algebra/Algebra/Epi.lean
feat: the rank of the ℤ-span of the roots of a root system is the dimension (#33846) …
Added Algebra.isEpi_iff_surjective_algebraMap_of_finiteView on Github →