Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-14 12:34 70ca6fd8

View on Github →

feat(ring_theory/power_basis): equivs between algebras with the same power basis (#4986) power_basis.lift and power_basis.equiv use the power basis structure to define alg_homs and alg_equivs.

The main application in this PR is power_basis.equiv_adjoin_simple, which states that adjoining an element of a power basis of L : K gives L itself.

Estimated changes

Modified src/data/polynomial/algebra_map.lean

added theorem polynomial.aeval_eq_sum_range'

added theorem polynomial.aeval_eq_sum_range

Modified src/data/polynomial/degree/basic.lean

added theorem polynomial.degree_add_eq_left_of_degree_lt

deleted theorem polynomial.degree_add_eq_of_degree_lt

added theorem polynomial.degree_add_eq_right_of_degree_lt

added theorem polynomial.degree_sub_eq_left_of_degree_lt

added theorem polynomial.degree_sub_eq_right_of_degree_lt

added theorem polynomial.degree_sum_fin_lt

Modified src/data/polynomial/div.lean

added theorem polynomial.eval₂_mod_by_monic_eq_self_of_root

Modified src/data/polynomial/eval.lean

added theorem polynomial.eval₂_eq_sum_range'

Modified src/data/polynomial/field_division.lean

Modified src/data/polynomial/lifts.lean

Modified src/data/polynomial/monic.lean

added theorem polynomial.monic_add_of_left

added theorem polynomial.monic_add_of_right

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.aeval_mod_by_monic_eq_self_of_root

Modified src/field_theory/minimal_polynomial.lean

modified theorem minimal_polynomial.ne_zero

Modified src/linear_algebra/char_poly/coeff.lean

Modified src/ring_theory/power_basis.lean

deleted theorem adjoin_root.findim

deleted theorem adjoin_root.finite_dimensional

added theorem intermediate_field.adjoin.power_basis.gen_eq

added theorem power_basis.aeval_minpoly_gen

added theorem power_basis.constr_pow_aeval

added theorem power_basis.constr_pow_algebra_map

added theorem power_basis.constr_pow_gen

added theorem power_basis.constr_pow_mul

added theorem power_basis.dim_le_nat_degree_of_root

added theorem power_basis.dim_ne_zero

added theorem power_basis.equiv_adjoin_simple_aeval

added theorem power_basis.equiv_adjoin_simple_gen

added theorem power_basis.equiv_adjoin_simple_symm_aeval

added theorem power_basis.equiv_adjoin_simple_symm_gen

added theorem power_basis.equiv_aeval

added theorem power_basis.equiv_gen

added theorem power_basis.equiv_symm

added theorem power_basis.exists_eq_aeval

added theorem power_basis.is_integral_gen

added theorem power_basis.lift_aeval

added theorem power_basis.lift_gen

added theorem power_basis.minpoly_gen_monic

added theorem power_basis.nat_degree_lt_nat_degree

added theorem power_basis.nat_degree_minimal_polynomial

added theorem power_basis.nat_degree_minpoly_gen