toEquiv_injective — Mathlib

English

The map that sends a semilinear equivalence to its underlying type equivalence is injective: if two semilinear equivalences have the same underlying equivalence, then they are equal.

Русский

Отображение, отправляющее семилинейную эквивалентность в соответствующую эквивалентность как множества, инъективно: если две такие эквивалентности имеют одинаковую базовую эквивалентность, то они равны.

LaTeX

$$Injective (toEquiv) : (M ≃ₛₗ[σ] M₂) → M ≃ M₂$$

Lean4

theorem toEquiv_injective : Function.Injective (toEquiv : (M ≃ₛₗ[σ] M₂) → M ≃ M₂) :=
  fun ⟨⟨⟨_, _⟩, _⟩, _, _, _⟩ ⟨⟨⟨_, _⟩, _⟩, _, _, _⟩ h ↦
  (LinearEquiv.mk.injEq _ _ _ _ _ _ _ _).mpr ⟨LinearMap.ext (congr_fun (Equiv.mk.inj h).1), (Equiv.mk.inj h).2⟩

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