rTensor_surjective_iff — Mathlib

English

Analogous surjectivity criterion for the right tensor: f.rTensor M is surjective iff f is surjective.

Русский

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

LaTeX

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

Lean4

theorem rTensor_surjective_iff {f : N →ₗ[R] P} : Function.Surjective (f.rTensor M) ↔ Function.Surjective f := by
  rw [← LinearMap.lTensor_surj_iff_rTensor_surj, lTensor_surjective_iff]

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