mathlib

4bfeb0d2 - chore(group_theory/submonoid/operations): use coercion instead of .val

chore(group_theory/submonoid/operations): use coercion instead of .val lemmas are generally phrased about coercions, so in the unlikely even this is unfolded, the former is more likely to be useful.