Commit 2020-09-30 18:14 23b04b0f
View on Github →chore(ring_theory/algebra): Mark algebra.mem_top as simp (#4339)
This is consistent with subsemiring.mem_top and submonoid.mem_top, both of which are marked simp.
chore(ring_theory/algebra): Mark algebra.mem_top as simp (#4339)
This is consistent with subsemiring.mem_top and submonoid.mem_top, both of which are marked simp.