Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alg_hom.normal_bijective

Modification history

2021-01-30 20:09
src/field_theory/normal.lean
feat(field_theory/normal): Restriction is surjective (#5960) …
Added alg_hom.normal_bijectiveView on Github →