mathlib

ae1b5302 - chore(algebra/algebra/basic): add simp lemma about `algebra_map ℚ` (#5970)

chore(algebra/algebra/basic): add simp lemma about `algebra_map ℚ` (#5970) Since there is a subsingleton instance over ring_homs, we may as well let the simplifier replace `algebra_map` with `id`.