Direct product of subgroups is abelian

Stream: mathlib4

[Move fast]

import Mathlib

open Subgroup

variable {n : ℕ}

variable {G : Fin n → Type*} [∀ i, Group (G i)]

instance  (h:CommGroup (Π i : Fin n, G i) ) :

∀ i : Fin n, CommGroup (G i) := by sorry

How can I construct this instance? I want to show that if the direct product of subgroups is abelian, then every direct factor is abelian.

[Aaron Liu]

I don't think this is provable this is provable, but needs some kind of choice

[Aaron Liu]

Since that statement doesn't mean what you say it does

[Move fast]

I have modified the edited content.

[Aaron Liu]

It is still not provable, and still does not say what you think it says

[Aaron Liu]

Maybe you can use docs#IsMulCommutative instead

[Move fast]

ok, thank you.

[Kevin Buzzard]

As I already told you once @Move fast , CommGroup X does not mean "the group X is commutative".

[Kevin Buzzard]

It is the type of commutative group structures on X.