equiv_symm_apply — Mathlib

English

The inverse of the base-change equivalence sends f(m) to 1 ⊗ m, recovering the base-change relation.

Русский

Обратное к базовому изменению отображение переводит f(m) в 1 ⊗ m, восстанавливая зависимость базового изменения.

LaTeX

$$$ h.equiv^{-1}(f(m)) = 1 \otimes m $$$

Lean4

theorem equiv_symm_apply (m : M) : h.equiv.symm (f m) = 1 ⊗ₜ m := by rw [h.equiv.symm_apply_eq, h.equiv_tmul, one_smul]

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