Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-01 12:12 e803c851

View on Github →

feat(field_theory/separable): relating irreducibility and separability (#3198)

Estimated changes

Modified src/data/polynomial.lean

added theorem polynomial.degree_derivative_le

added theorem polynomial.degree_derivative_lt

added theorem polynomial.derivative_eval₂_C

added theorem polynomial.derivative_map

added theorem polynomial.derivative_pow

added theorem polynomial.derivative_pow_succ

added theorem polynomial.eval₂_nat_cast

added theorem polynomial.is_unit_iff

added theorem polynomial.map_nat_cast

added theorem polynomial.nat_degree_derivative_lt

added theorem polynomial.nat_degree_le_of_dvd

added theorem polynomial.of_mem_support_derivative

Modified src/field_theory/separable.lean

added theorem irreducible.separable

added theorem polynomial.coe_expand

added theorem polynomial.coeff_contract

added theorem polynomial.coeff_expand

added theorem polynomial.coeff_expand_mul'

added theorem polynomial.coeff_expand_mul

added theorem polynomial.derivative_expand

added theorem polynomial.exists_separable_of_irreducible

added theorem polynomial.expand_C

added theorem polynomial.expand_X

added theorem polynomial.expand_contract

added theorem polynomial.expand_eq_C

added theorem polynomial.expand_eq_map_domain

added theorem polynomial.expand_eq_zero

added theorem polynomial.expand_expand

added theorem polynomial.expand_inj

added theorem polynomial.expand_monomial

added theorem polynomial.expand_mul

added theorem polynomial.expand_one

added theorem polynomial.expand_pow

added theorem polynomial.is_local_ring_hom_expand

added theorem polynomial.is_unit_or_eq_zero_of_separable_expand

added theorem polynomial.nat_degree_expand

added theorem polynomial.of_irreducible_expand

added theorem polynomial.of_irreducible_expand_pow

added theorem polynomial.separable.is_coprime

added theorem polynomial.separable.map

added theorem polynomial.separable.of_pow'

added theorem polynomial.separable.of_pow

added theorem polynomial.separable_C

added theorem polynomial.separable_iff_derivative_ne_zero

added theorem polynomial.separable_or

added theorem polynomial.unique_separable_of_irreducible

Modified src/ring_theory/algebra.lean

added theorem alg_hom.map_nat_cast

Modified src/ring_theory/ideals.lean

added theorem of_irreducible_map

Modified src/ring_theory/polynomial/basic.lean