Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-19 01:03 eb22ba4f

View on Github →

chore(algebra/monoid_algebra/basic): use the homomorphism typeclasses (#13389) This replaces mul_hom with mul_hom_class and add_hom with add_hom_class. Also adds two trivial lemmas, monoid_algebra.map_domain_one and add_monoid_algebra.map_domain_one.

Estimated changes