lTensor_surjective_iff — Mathlib

English

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

Русский

Для любого f: N → P, f.lTensor MSurjective эквивалентно f surjective.

LaTeX

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

Lean4

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

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