mathlib

23b04b0f - chore(ring_theory/algebra): Mark algebra.mem_top as simp (#4339)

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.