tensorKer_tmul — Mathlib

English

There is an isomorphism between M ⊗ ker f and ker(lTensor S M f), i.e., tensoring with M preserves the kernel structure of f.

Русский

Существует изоморфизм между M ⊗ ker f и ker(lTensor S M f), то есть тензорирование на M сохраняет структуру ядра f.

LaTeX

$$$\text{tensorKerEquiv} : M ⊗_R ker f \cong_S ker( lTensor\; S\; M\; f )$$$

Lean4

@[simp]
theorem tensorKer_tmul (m : M) (x : LinearMap.ker f) : (tensorKer S M f (m ⊗ₜ[R] x) : M ⊗[R] N) = m ⊗ₜ[R] (x : N) :=
  rfl

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