Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-30 17:07 0eb9db6a

View on Github →

chore(linear_algebra/multivariate_polynomial): move rename to the right place

Estimated changes

Modified src/data/equiv/algebra.lean

deleted theorem mv_polynomial.hom_eq_hom

deleted theorem mv_polynomial.is_id

deleted def mv_polynomial.rename

deleted theorem mv_polynomial.rename_C

deleted theorem mv_polynomial.rename_X

deleted theorem mv_polynomial.rename_id

deleted theorem mv_polynomial.rename_rename

Modified src/linear_algebra/multivariate_polynomial.lean

added theorem mv_polynomial.hom_eq_hom

added theorem mv_polynomial.is_id

added def mv_polynomial.rename

added theorem mv_polynomial.rename_C

added theorem mv_polynomial.rename_X

added theorem mv_polynomial.rename_id

added theorem mv_polynomial.rename_rename