right — Mathlib

English

If M is invertible, then the dual module Dual_R(M) is invertible as an R-module.

Русский

Если M обратим, то дуальный модуль Dual_R(M) является обратимым как R-модуль.

LaTeX

$$Module.Invertible R (Dual_R(M))$$

Lean4

protected theorem right : Module.Invertible R N where
  bijective :=
    by
    rw [show contractLeft R N = ((linearEquivDual e).rTensor N).symm ≪≫ₗ e by
        rw [LinearEquiv.coe_trans, LinearEquiv.eq_comp_toLinearMap_symm]; ext; rfl]
    apply LinearEquiv.bijective

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