Commit 2023-05-23 16:17 c82f1498

View on Github →

feat: port FieldTheory.Separable (#4272)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Separable.lean

added theorem AlgHom.card_of_powerBasis

added theorem Irreducible.separable

added theorem IsSeparable.isIntegral

added theorem IsSeparable.of_algHom

added theorem IsSeparable.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.isCoprime

added theorem Polynomial.Separable.map

added theorem Polynomial.Separable.mul

added theorem Polynomial.Separable.of_dvd

added theorem Polynomial.Separable.of_mul_left

added theorem Polynomial.Separable.of_mul_right

added theorem Polynomial.Separable.of_pow'

added theorem Polynomial.Separable.of_pow

added theorem Polynomial.Separable.squarefree

added def Polynomial.Separable

added theorem Polynomial.X_pow_sub_one_separable_iff

added theorem Polynomial.card_rootSet_eq_natDegree

added theorem Polynomial.count_roots_le_one

added theorem Polynomial.eq_X_sub_C_of_separable_of_root_eq

added theorem Polynomial.exists_finset_of_splits

added theorem Polynomial.exists_separable_of_irreducible

added theorem Polynomial.isUnit_of_self_mul_dvd_separable

added theorem Polynomial.isUnit_or_eq_zero_of_separable_expand

added theorem Polynomial.multiplicity_le_one_of_separable

added theorem Polynomial.nodup_of_separable_prod

added theorem Polynomial.nodup_roots

added theorem Polynomial.not_separable_zero

added theorem Polynomial.rootMultiplicity_le_one_of_separable

added theorem Polynomial.separable_C

added theorem Polynomial.separable_X

added theorem Polynomial.separable_X_add_C

added theorem Polynomial.separable_X_pow_sub_C

added theorem Polynomial.separable_X_pow_sub_C_unit

added theorem Polynomial.separable_X_sub_C

added theorem Polynomial.separable_def'

added theorem Polynomial.separable_def

added theorem Polynomial.separable_gcd_left

added theorem Polynomial.separable_gcd_right

added theorem Polynomial.separable_iff_derivative_ne_zero

added theorem Polynomial.separable_map

added theorem Polynomial.separable_of_subsingleton

added theorem Polynomial.separable_one

added theorem Polynomial.separable_or

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

added theorem Polynomial.unique_separable_of_irreducible

added theorem isSeparable_iff

added theorem isSeparable_tower_bot_of_isSeparable

added theorem isSeparable_tower_top_of_isSeparable