lTensor_bijective_iff — Mathlib

English

For invertible M, f.lTensor M is bijective iff f is bijective.

Русский

Для обратимого M отображение f.lTensor M биективно тогда и только тогда, когда f биективно.

LaTeX

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

Lean4

theorem lTensor_bijective_iff {f : N →ₗ[R] P} : Function.Bijective (f.lTensor M) ↔ Function.Bijective f := by
  simp_rw [Function.Bijective, lTensor_injective_iff, lTensor_surjective_iff]

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