Commutator subgroup (aka Derived subgroup)

Stream: Is there code for X?

[Antoine Chambert-Loir]

For Group G, the derived subgroup (or commutator subgroup) is the Subgroup G generated by all commutators of elements of G. It can be obtained either by
_root_.commutator G, Subgroup.commutator (G := (⊤ : Subgroup G)), or even derivedSeries G 1.
The third way rewrites (using simp) to the first one, but the first one is not easy to use under open Subgroup.

Could Subgroup.commutator be protected?
Or could _root_.commutator be renamed as Commutator?

[Eric Wieser]

docs#commutator, docs#Subgroup.commutator

[Eric Wieser]

docs#Subgroup.commutator should be renamed to Subgroup.instBracket in my opinion

[Eric Wieser]

(note it was automatically protected in Lean 3 due to being an instance)