ofTensorProductEquivOfFiniteNoetherian_apply

English

For finite module M, the equiv of finite Noetherian coincides with the basic tensor product map.

Русский

Для конечного модуля M эквивалентность конечного Ноетерова совпадает с базовым тензорным отображением.

LaTeX

$$$\bigl(\mathrm{AdicCompletion.ofTensorProductEquivOfFiniteNoetherian}\ I\ M\bigr)\; \text{symm applied to }(\mathrm{of I M}\ x) = 1 \otimes x$$$

Lean4

@[simp]
theorem ofTensorProductEquivOfFiniteNoetherian_apply [Module.Finite R M] (x : AdicCompletion I R ⊗[R] M) :
    ofTensorProductEquivOfFiniteNoetherian I M x = ofTensorProduct I M x :=
  rfl

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