equiv_tmul — Mathlib

English

Base change is equivalent to the existence of a suitable linear equivalence that exhibits N ≅_S S ⊗_R M.

Русский

Базовое изменение эквивалентно существованию соответствующего линейного эквивалента, показывающего N ≅_S S ⊗_R M.

LaTeX

$$$ IsBaseChange S f \iff \exists e: (TensorProduct R S M) \to N, e \text{ is an S-linear equivalence with } e(1 \otimes m) = f(m) $$$

Lean4

theorem equiv_tmul (s : S) (m : M) : h.equiv (s ⊗ₜ m) = s • f m :=
  rfl

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