∀ {R : Type u} {M₁ : Type v} {M₂ : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] (e : M₁ ≃ₗ[R] M₂), e.lieConj.symm = e.symm.lieConj