fixing_subgroup etc.

Stream: maths

[Antoine Chambert-Loir]

The branch#acl-fixing_subgroup proposes a file that gives some lemmas related to the fixing subgroup (resp fixing submonoid) in the context of a mul_action.
Is it relevant to ask for some review before I create a pull request? The definition is already as docs#fixing_subgroup and needs to be deleted from there.
Some lemmas related to docs#antitone.dual etc. have been extended as iff-lemmas.

[Johan Commelin]

I see two lemmas that are commented out. But otherwise a superficial look suggests that this is ready for a PR and a more thorough review.

[Antoine Chambert-Loir]

OK, I just pushed #13202.