lTensor_surj_iff_rTensor_surj — Mathlib

English

Bijectivity and surjectivity across lTensor and rTensor remain equivalent under linear equivalences.

Русский

Биективность и сюръективность сохраняются при применении линейных эквивалентностей к lTensor и rTensor.

LaTeX

$$$ \\mathrm{Bijective}(lTensor M f) \\iff \\mathrm{Bijective}(rTensor M f) $$$

Lean4

/-- Given a linear map `f : N → P`, `f ⊗ M` is surjective if and only if `M ⊗ f` is surjective. -/
theorem lTensor_surj_iff_rTensor_surj : Function.Surjective (lTensor M f) ↔ Function.Surjective (rTensor M f) := by
  simp [← comm_comp_rTensor_comp_comm_eq]

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