Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-24 13:03 579b142d

View on Github →

feat(field_theory/fixed): a field is normal over the fixed subfield under a group action (#3520) From my Galois theory repo.

Estimated changes

added theorem list.smul_prod
added theorem multiset.smul_prod
modified theorem polynomial.coeff_smul'
added theorem polynomial.eval_smul'
modified theorem polynomial.smul_C
modified theorem polynomial.smul_X
added theorem polynomial.smul_eval
added theorem prod_X_sub_smul.coeff
added theorem prod_X_sub_smul.eval
added theorem prod_X_sub_smul.monic
added theorem prod_X_sub_smul.smul
added theorem smul_prod
deleted theorem smul_neg
deleted theorem smul_sub
added theorem polynomial.map_dvd_map
added theorem fixed_points.smul
added theorem normal.is_integral
added theorem normal.splits
added def normal
added theorem smul_neg
added theorem smul_sub
added theorem algebra.coe_top