Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monoid_algebra.map_domain_one

Modification history

2022-04-19 01:03
src/algebra/monoid_algebra/basic.lean
chore(algebra/monoid_algebra/basic): use the homomorphism typeclasses (#13389) …
Added monoid_algebra.map_domain_oneView on Github →