Commit 2021-01-30 22:44 ae1b5302
View on Github →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.
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.