Theorem IsAlgClosed.ringHom_bijective_of_isIntegral

Modification history

2025-05-01 06:42
Mathlib/FieldTheory/IsAlgClosed/Basic.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Added IsAlgClosed.ringHom_bijective_of_isIntegralView on Github →