feat(field_theory/normal): Restriction is surjective (#5960)
Proves surjectivity of `alg_equiv.restrict_normal_hom`.
Also proves a bijectivity lemma which gives a cleaner construction of `alg_equiv.restrict_normal`.
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
