mathlib

34302c63 - chore(ring_theory/algebra): add comments explaining absence of 2 `simp` attrs (#3002)