Commit 2023-06-09 16:56 8d243ee8

View on Github →

feat: port FieldTheory.Fixed (#4890)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Fixed.lean

added def FixedBy.subfield

added theorem FixedPoints.coe_algebraMap

added theorem FixedPoints.finrank_eq_card

added theorem FixedPoints.finrank_le_card

added theorem FixedPoints.isIntegral

added theorem FixedPoints.linearIndependent_smul_of_linearIndependent

added theorem FixedPoints.minpoly.eval₂'

added theorem FixedPoints.minpoly.eval₂

added theorem FixedPoints.minpoly.irreducible

added theorem FixedPoints.minpoly.irreducible_aux

added theorem FixedPoints.minpoly.monic

added theorem FixedPoints.minpoly.ne_one

added theorem FixedPoints.minpoly.of_eval₂

added def FixedPoints.minpoly

added theorem FixedPoints.minpoly_eq_minpoly

added theorem FixedPoints.rank_le_card

added theorem FixedPoints.smul

added theorem FixedPoints.smul_polynomial

added def FixedPoints.subfield

added def FixedPoints.toAlgHomEquiv

added theorem FixedPoints.toAlgHom_bijective

added theorem cardinal_mk_algHom

added theorem finrank_algHom

added theorem linearIndependent_toLinearMap