Theorem AlgEquiv.card_le

Modification history

2025-04-25 07:04
Mathlib/FieldTheory/Fixed.lean
feat(FieldTheory): add the class `IsQuadraticExtension` (#24114)
Added AlgEquiv.card_leView on Github →