mathlib
ecf18c69 - refactor(field_theory/minimal_polynomial, *): make `aeval`, `is_integral`, and `minimal_polynomial` noncommutative (#4001)

Commit
5 years ago
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'`
Author
Parents
Loading