mathlib3

593938cd - 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 (#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>