Commit 2021-10-24 00:37 d788647f

View on Github →

feat(ring_theory): generalize adjoin_root.power_basis (#9536) Now we only need that g is monic to state that adjoin_root g has a power basis. Note that this does not quite imply the result of #9529: this is phrased in terms of minpoly R (root g) and the other PR in terms of g itself, so I don't have a direct use for the current PR. However, it seems useful enough to have this statement, so I PR'd it anyway.

Estimated changes

Modified src/data/polynomial/div.lean

added theorem polynomial.sum_fin

added theorem polynomial.sum_mod_by_monic_coeff

Modified src/ring_theory/adjoin_root.lean

added theorem adjoin_root.is_integral_root'

added theorem adjoin_root.mk_eq_mk

added theorem adjoin_root.mk_left_inverse

added theorem adjoin_root.mk_surjective

added def adjoin_root.mod_by_monic_hom

added theorem adjoin_root.mod_by_monic_hom_mk

added def adjoin_root.power_basis'

added def adjoin_root.power_basis_aux'