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`.

Author: eric-wieser

src/algebra/algebra/basic.lean

@@ -1013,6 +1013,9 @@ namespace rat
 instance algebra_rat {α} [division_ring α] [char_zero α] : algebra ℚ α :=
 (rat.cast_hom α).to_algebra' $ λ r x, r.cast_commute x
 
+@[simp] theorem algebra_map_rat_rat : algebra_map ℚ ℚ = ring_hom.id ℚ :=
+subsingleton.elim _ _
+
 end rat
 
 namespace algebra