mathlib
a2630fc3 - chore(field_theory|ring_theory|linear_algebra): rename minimal_polynomial to minpoly (#5771)

Commit
4 years ago
chore(field_theory|ring_theory|linear_algebra): rename minimal_polynomial to minpoly (#5771) This PR renames: * `minimal_polynomial` -> `minpoly` * a similar substitution throughout the library for all names containing the substring `minimal_polynomial` * `fixed_points.minpoly.minimal_polynomial` -> `fixed_points.minpoly_eq_minpoly` This PR moves a file: src/field_theory/minimal_polynomial.lean -> src/field_theory/minpoly.lean Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Author
Parents
Loading