toLinearEquiv_injective — Mathlib

English

If two Lie equivalences have the same underlying Lie algebra homomorphism, then they are equal.

Русский

Если две эквиваленты Ли имеют одинаковую основанную на гомоморфизме Ли отображение, они равны между собой.

LaTeX

$$$ (e_1 : L_1 \simeq_R L_2) = (e_2 : L_1 \simeq_R L_2) \\Rightarrow e_1 = e_2 $$$

Lean4

theorem toLinearEquiv_injective : Injective ((↑) : (L₁ ≃ₗ⁅R⁆ L₂) → L₁ ≃ₗ[R] L₂) :=
  by
  rintro ⟨⟨⟨⟨f, -⟩, -⟩, -⟩, f_inv⟩ ⟨⟨⟨⟨g, -⟩, -⟩, -⟩, g_inv⟩
  simp

Похожие утверждения