Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-01 04:51 12763ecc

View on Github →

chore(*): more use of bundled ring homs (#4012)

Estimated changes

Modified src/data/list/basic.lean

modified theorem list.prod_hom

Modified src/data/multiset/basic.lean

modified theorem multiset.prod_hom

Modified src/data/polynomial/eval.lean

Modified src/ring_theory/ideal/operations.lean