Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alg_equiv.lift_normal_commutes

Modification history

2022-06-02 19:38
src/field_theory/normal.lean
refactor(field_theory/normal): generalize `lift_normal` and `restrict_normal` (#14450) …
Modified alg_equiv.lift_normal_commutesView on Github →
2021-01-30 20:09
src/field_theory/normal.lean
feat(field_theory/normal): Restriction is surjective (#5960) …
Added alg_equiv.lift_normal_commutesView on Github →