Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-30 05:41 03c302dc

View on Github →

feat(field_theory/fixed): field is separable over fixed subfield under group action (#3568)

Estimated changes

Modified src/data/polynomial/field_division.lean

added theorem polynomial.gcd_map

added theorem polynomial.is_coprime_map

added theorem polynomial.is_unit_map

Modified src/field_theory/fixed.lean

Modified src/field_theory/separable.lean

added def is_separable

added theorem polynomial.separable.inj_of_prod_X_sub_C

added theorem polynomial.separable.injective_of_prod_X_sub_C

added theorem polynomial.separable_X_sub_C

added theorem polynomial.separable_map

added theorem polynomial.separable_prod'

added theorem polynomial.separable_prod

added theorem polynomial.separable_prod_X_sub_C_iff'

added theorem polynomial.separable_prod_X_sub_C_iff