Theorem normal_of_finrank_eq_two

Modification history

2025-04-25 07:04

Mathlib/FieldTheory/Normal/Basic.lean

feat(FieldTheory): add the class `IsQuadraticExtension` (#24114)

Deleted normal_of_finrank_eq_two View on Github →

2025-04-07 10:22

Mathlib/FieldTheory/Normal/Basic.lean

feat(FieldTheory/Normal): A quadratic extension is normal (#23452)

Added normal_of_finrank_eq_two View on Github →