…hat the induction tactic accepts them

This was causing notation overload problems with module smul

…roup on is_submonoid

… closure

…ne in group theory

…ercase names, ...)

…left_coset

…a sum to the sum of all combinations)

Fixed also a typo pointed out by Scott

…ass_eq_left_coset is now a theorem

based on Zulip conversations and requests