toLinearMap_injective — Mathlib

English

The forgetful map from semilinear equivalences to their underlying linear maps is injective: if two semilinear equivalences have the same underlying linear map, they are equal.

Русский

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

LaTeX

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

Lean4

theorem toLinearMap_injective : Injective (toLinearMap : (M ≃ₛₗ[σ] M₂) → M →ₛₗ[σ] M₂) := fun _ _ H ↦
  toEquiv_injective <| Equiv.ext <| LinearMap.congr_fun H

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