instModuleIsReflexive — Mathlib

English

The isomorphism between a module and its MulOpposite preserves reflexivity: if M is IsReflexive, then MulOpposite M is IsReflexive.

Русский

Изоморфизм между модулем и его MulOpposite сохраняет рефлексивность: если M рефлексивен, то MulOpposite M также рефлексивен.

LaTeX

$$IsReflexive(R,M) \\Rightarrow IsReflexive(R, MulOpposite M).$$

Lean4

instance _root_.MulOpposite.instModuleIsReflexive : IsReflexive R (MulOpposite M) :=
  equiv <|
    MulOpposite.opLinearEquiv
      _
        -- see Note [lower instance priority]

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