Theorem AlgEquiv.restrictNormalHom_apply

Modification history

2025-01-23 18:20
Mathlib/FieldTheory/Normal/Basic.lean
refactor(FieldTheory/Normal): Split file (#20724) …
Modified AlgEquiv.restrictNormalHom_applyView on Github →
2024-12-01 09:31
Mathlib/FieldTheory/Normal.lean
feat(FieldTheory/Galois): Lemmas of galois theory (#16979) …
Added AlgEquiv.restrictNormalHom_applyView on Github →