equiv_symm_apply — Mathlib

English

Applying lift.equiv and then evaluating on a simple tensor yields the same result as applying the original bilinear map.

Русский

Применение lift.equiv и последующая проверка на простом тензоре дают тот же результат, что и исходное билинейное отображение.

LaTeX

$$$\\mathrm{equiv\\_apply}\\ (f)\\ (m)\\ (n) = f\\ m\\ n.$$$

Lean4

@[simp]
theorem equiv_symm_apply (f : M ⊗[R] N →ₗ[R] P) (m : M) (n : N) : (lift.equiv R M N P).symm f m n = f (m ⊗ₜ n) :=
  rfl

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