linearEquivOfInjective_apply — Mathlib

English

If f is a linear map with finite-dimensional domain and codomain, hf is injective and hdim holds, then the constructed linear equivalence acts as f on every x.

Русский

Если f — линейное отображение между конечномерными пространствами, hf инъективно и выполняется равенство размерностей, то построенное линейное эквивалентное отображение совпадает с f на каждом аргументе.

LaTeX

$$$ f.linearEquivOfInjective hf hdim x = f x $$$

Lean4

@[simp]
theorem linearEquivOfInjective_apply [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂}
    (hf : Injective f) (hdim : finrank K V = finrank K V₂) (x : V) : f.linearEquivOfInjective hf hdim x = f x :=
  rfl

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