algebra): add missing rfl lemmas (#8924)

Commit

4 years ago

chore(algebra/direct_sum/algebra): add missing rfl lemmas (#8924) I realized I was resorting to nasty unfolding to get these mid-proof

Author

eric-wieser

Parents