Commit 2019-05-20 15:11 593938cd
View on Github →chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map (#1062)
- chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map From the perfectoid project.
- Stupid error
- Update src/ring_theory/algebra.lean Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com