mathlib3

158724c8 - feat(group_theory/subgroup/basic): Multiplication of disjoint subgroups is injective (#16966)

feat(group_theory/subgroup/basic): Multiplication of disjoint subgroups is injective (#16966) This PR proves that if `H₁` and `H₂` are disjoint subgroups of `G`, then the multiplication map `H₁ × H₂ → G` is injective. This is useful for a couple results about complementary subgroups.