Commit 2020-09-04 00:52 ecf18c69

View on Github →

refactor(field_theory/minimal_polynomial, *): make aeval, is_integral, and minimal_polynomial noncommutative (#4001) Makes aeval, is_integral, and minimal_polynomial compatible with noncommutative algebras Renames eval₂_ring_hom_noncomm to eval₂_ring_hom'

Estimated changes

Modified src/data/polynomial/algebra_map.lean

Modified src/data/polynomial/eval.lean

modified theorem polynomial.eval₂_list_prod_noncomm

modified theorem polynomial.eval₂_mul_noncomm

added def polynomial.eval₂_ring_hom'

deleted def polynomial.eval₂_ring_hom_noncomm

Modified src/field_theory/minimal_polynomial.lean

Modified src/linear_algebra/eigenspace.lean

added theorem module.End.ker_eval₂_ring_hom'_unit_polynomial

deleted theorem module.End.ker_eval₂_ring_hom_noncomm_unit_polynomial

Modified src/ring_theory/algebraic.lean

Modified src/ring_theory/integral_closure.lean

deleted theorem is_integral_of_noetherian'

modified theorem is_integral_of_noetherian

added theorem is_integral_of_submodule_noetherian