mathlib

0487a1d2 - chore(algebra/algebra/basic): fix definition of `ring_hom.to_algebra` (#4561)

chore(algebra/algebra/basic): fix definition of `ring_hom.to_algebra` (#4561) The new definition uses `to_ring_hom := i` instead of `.. i` to get defeq `algebra_map R S = i`, and adds it as a lemma.