Commit 2022-03-12 14:08 b9ab27bd
View on Github →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.