rTensor_injective_iff — Mathlib

English

Similarly, for f: N → P, f.rTensor M is injective iff f is injective.

Русский

Аналогично, f.rTensor M инъективен тогда и только тогда, когда f инъективен.

LaTeX

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

Lean4

theorem rTensor_injective_iff {f : N →ₗ[R] P} : Function.Injective (f.rTensor M) ↔ Function.Injective f := by
  rw [← LinearMap.lTensor_inj_iff_rTensor_inj, lTensor_injective_iff]

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