Commit 2025-04-25 07:04 7d8506d1

View on Github →

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

Estimated changes

Modified Mathlib/FieldTheory/Fixed.lean

added theorem AlgEquiv.card_le

added theorem AlgHom.card_le

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/FieldTheory/Normal/Basic.lean

deleted theorem normal_of_finrank_eq_two

Modified Mathlib/LinearAlgebra/Dimension/Finrank.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean