coe_ofTensorProductEquivOfFiniteNoetherian

English

In the finite-Noetherian setting, the linear map underlying the finite-Noetherian equivalence equals the canonical tensor map.

Русский

В конечной ноетеровой ситуации линейное отображение, лежащее в основе эквивалентности, равно каноническому тензорному отображению.

LaTeX

$$$\bigl(\mathrm{AdicCompletion.ofTensorProductEquivOfFiniteNoetherian}\ I\ M\bigr).toLinearMap = \mathrm{ofTensorProduct}\ I\ M$$$

Lean4

theorem coe_ofTensorProductEquivOfFiniteNoetherian [Module.Finite R M] :
    ofTensorProductEquivOfFiniteNoetherian I M = ofTensorProduct I M :=
  rfl

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