rTensor_comp_flip_mk — Mathlib

English

Dual bijectivity: lTensor M f is bijective if and only if rTensor M f is bijective.

Русский

Двойственная биекция: lTensor M f биективно тогда и только тогда, когда rTensor M f биективно.

LaTeX

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

Lean4

@[simp]
theorem rTensor_comp_flip_mk (m : M) :
    f.rTensor M ∘ₗ (TensorProduct.mk R N M).flip m = (TensorProduct.mk R P M).flip m ∘ₗ f :=
  rfl

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