Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-10 23:30 5c9e3ef8

View on Github →

feat(ring_theory/adjoin_root): Dimension of adjoin_root (#4830) Adds adjoin_root.degree_lt_linear_equiv, the restriction of adjoin_root.mk f to the polynomials of degree less than f, viewed as a isomorphism between vector spaces over K and uses it to prove that adjoin_root f has dimension f.nat_degree. Also renames adjoin_root.alg_hom to adjoin_root.lift_hom.

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_equiv.map_pow

Modified src/field_theory/adjoin.lean

added theorem intermediate_field.adjoin_root_equiv_adjoin_apply_root

added theorem intermediate_field.aeval_gen_minimal_polynomial

Modified src/field_theory/splitting_field.lean

Modified src/ring_theory/adjoin_root.lean

added theorem adjoin_root.aeval_alg_hom_eq_zero

deleted def adjoin_root.alg_hom

deleted theorem adjoin_root.coe_alg_hom

added theorem adjoin_root.coe_lift_hom

added def adjoin_root.equiv

added def adjoin_root.lift_hom

added theorem adjoin_root.lift_hom_eq_alg_hom

Modified src/ring_theory/power_basis.lean

added theorem adjoin_root.findim

added theorem adjoin_root.finite_dimensional

modified theorem adjoin_root.power_basis_is_basis

added theorem intermediate_field.adjoin.findim

added theorem intermediate_field.adjoin.finite_dimensional

deleted theorem intermediate_field.adjoin_simple.exists_eq_aeval_gen

modified theorem intermediate_field.power_basis_is_basis

added theorem power_basis.findim

modified theorem power_basis.finite_dimensional