English
Two subgroups H and K of G are complements if the map (h,k) ↦ h k from H × K to G is bijective.
Русский
Две подгруппы H и K группы G являются дополнениями, если отображение (h,k) ↦ hk из H × K в G биективно.
LaTeX
$$$ \text{IsComplement}(H,K) \iff \text{Bijective} \big( (h,k) \mapsto h k \big) : H \times K \to G. $$$
Lean4
/-- `S` and `T` are complements if `(*) : S × T → G` is a bijection.
This notion generalizes left transversals, right transversals, and complementary subgroups.
If `S` and `T` are `SetLike`s such as `Subgroup`s, see `isComplement_iff_bijective` for a
more ergonomic way to unfold.
-/
@[to_additive /-- `S` and `T` are complements if `(+) : S × T → G` is a bijection
If `S` and `T` are `SetLike`s such as `AddSubgroup`s, see `isComplement_iff_bijective` for a
more ergonomic way to unfold. -/
]
def IsComplement : Prop :=
Function.Bijective fun x : S × T => x.1.1 * x.2.1
