English
If H and K are complements, then K and H are complements as well.
Русский
Если H и K являются дополнениями, то и K и H являются дополнениями.
LaTeX
$$$ \text{IsComplement'}(H,K) \Rightarrow \text{IsComplement'}(K,H). $$$
Lean4
@[to_additive]
theorem symm (h : IsComplement' H K) : IsComplement' K H :=
by
let ϕ : H × K ≃ K × H :=
Equiv.mk (fun x => ⟨x.2⁻¹, x.1⁻¹⟩) (fun x => ⟨x.2⁻¹, x.1⁻¹⟩) (fun x => Prod.ext (inv_inv _) (inv_inv _)) fun x =>
Prod.ext (inv_inv _) (inv_inv _)
let ψ : G ≃ G := Equiv.mk (fun g : G => g⁻¹) (fun g : G => g⁻¹) inv_inv inv_inv
suffices hf : (ψ ∘ fun x : H × K => x.1.1 * x.2.1) = (fun x : K × H => x.1.1 * x.2.1) ∘ ϕ by
rwa [isComplement'_def, isComplement_iff_bijective, ← Equiv.bijective_comp ϕ, ← hf, ψ.comp_bijective]
exact funext fun x => mul_inv_rev _ _
