Theorem IsAlgClosed.algebraMap_surjective_of_isIntegral
Modification history
2025-05-01 06:42
Mathlib/FieldTheory/IsAlgClosed/Basic.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Deleted IsAlgClosed.algebraMap_surjective_of_isIntegralView on Github →