lTensor_injective_iff — Mathlib

English

For any f: N → P, f.lTensor M is injective iff f is injective.

Русский

Для любого f: N → P, f.lTensor M инъективен тогда и только тогда, когда f инъективен.

LaTeX

$$Function.Injective (f.lTensor M) ↔ Function.Injective f$$

Lean4

theorem lTensor_injective_iff {f : N →ₗ[R] P} : Function.Injective (f.lTensor M) ↔ Function.Injective f :=
  by
  refine ⟨fun h ↦ ?_, Flat.lTensor_preserves_injective_linearMap _⟩
  rw [← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f]
  simpa using Flat.lTensor_preserves_injective_linearMap _ h

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