mathlib
9538e774 - refactor(algebra/direct_sum): unbundle `direct_sum.of`

Commit
4 years ago
refactor(algebra/direct_sum): unbundle `direct_sum.of` If this is bundled into an `add_monoid_hom`, then `simp` is not able to rewrite `of _ i (f j)` into `of _ j (f j)`, because it doesn't know how to rewrite the `add_monoid` term that is part of the type. In practice this change isn't too annoying elsewhere, as all we need are a few rewrites by the `of_add_hom_apply` lemma.
Author
Parents
Loading