Theorem AlgEquiv.restrictNormalHom_id

Modification history

2025-01-23 18:20

Mathlib/FieldTheory/Normal/Basic.lean

refactor(FieldTheory/Normal): Split file (#20724) …

Modified AlgEquiv.restrictNormalHom_id View on Github →

2024-10-18 17:54

Mathlib/FieldTheory/Normal.lean

feat(FieldTheory/Galois): Finite galois subextensions (#16978) …

Added AlgEquiv.restrictNormalHom_id View on Github →