mathlib3

b9ab27bd - feat(group_theory/subgroup/basic): add eq_one_of_noncomm_prod_eq_one_of_independent (#12525)

feat(group_theory/subgroup/basic): add eq_one_of_noncomm_prod_eq_one_of_independent (#12525) `finset.noncomm_prod` is “injective” in `f` if `f` maps into independent subgroups. It generalizes (one direction of) `subgroup.disjoint_iff_mul_eq_one`.