Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-03 22:00 f1637e56

View on Github →

feat(field_theory/splitting_field): definition of splitting field (#3272)

Estimated changes

Modified src/data/polynomial.lean

added theorem polynomial.X_dvd_iff

added theorem polynomial.X_sub_C_ne_zero

added theorem polynomial.irreducible_X

added theorem polynomial.irreducible_X_sub_C

added theorem polynomial.nat_degree_X

added theorem polynomial.nat_degree_X_le

modified theorem polynomial.nat_degree_X_sub_C

added theorem polynomial.nat_degree_div_by_monic

added theorem polynomial.nat_degree_le_nat_degree

modified theorem polynomial.nat_degree_le_of_degree_le

added theorem polynomial.not_is_unit_X

added theorem polynomial.not_is_unit_X_sub_C

added theorem polynomial.prime_X

added theorem polynomial.prime_X_sub_C

added theorem polynomial.root_mul

added theorem polynomial.roots_X_sub_C

added theorem polynomial.roots_mul

Modified src/field_theory/splitting_field.lean

added theorem polynomial.X_sub_C_mul_remove_factor

added def polynomial.factor

added theorem polynomial.factor_dvd_of_degree_ne_zero

added theorem polynomial.factor_dvd_of_nat_degree_ne_zero

added theorem polynomial.factor_dvd_of_not_is_unit

added theorem polynomial.nat_degree_remove_factor'

added theorem polynomial.nat_degree_remove_factor

added def polynomial.remove_factor

added theorem polynomial.splits_of_splits_of_dvd

added theorem polynomial.splitting_field.adjoin_roots

added def polynomial.splitting_field.lift

added def polynomial.splitting_field

added theorem polynomial.splitting_field_aux.adjoin_roots

added theorem polynomial.splitting_field_aux.algebra_map_succ

added theorem polynomial.splitting_field_aux.exists_lift

added theorem polynomial.splitting_field_aux.succ

added def polynomial.splitting_field_aux

Modified src/ring_theory/adjoin_root.lean

added theorem adjoin_root.adjoin_root_eq_top

added theorem adjoin_root.aeval_eq

added theorem adjoin_root.algebra_map_eq

added theorem adjoin_root.induction_on

added theorem adjoin_root.lift_comp_of

modified theorem adjoin_root.lift_root

added theorem adjoin_root.mk_X

Modified src/ring_theory/algebra.lean

added theorem algebra.comap_top

added theorem algebra.map_bot

added theorem algebra.map_top

added def subalgebra.comap'

added def subalgebra.map

added theorem subalgebra.map_le

Created src/ring_theory/algebra_tower.lean

added theorem algebra.adjoin_algebra_map'

added theorem algebra.adjoin_algebra_map

added theorem is_algebra_tower.algebra.ext

added theorem is_algebra_tower.algebra_map_apply

added theorem is_algebra_tower.algebra_map_eq

added theorem is_algebra_tower.comap_eq

added theorem is_algebra_tower.of_algebra_map_eq

added theorem is_algebra_tower.range_under_adjoin

added def is_algebra_tower.subalgebra_comap

added theorem is_algebra_tower.subalgebra_comap_top

added def is_algebra_tower.to_alg_hom

Modified src/ring_theory/polynomial/basic.lean

added theorem polynomial.exists_irreducible_of_degree_pos

added theorem polynomial.exists_irreducible_of_nat_degree_ne_zero

added theorem polynomial.exists_irreducible_of_nat_degree_pos