reflexive_right — Mathlib

English

Dualizing the previous pairing on the other side shows that N is reflexive as an R-module when p is a perfect pairing between M and N.

Русский

Дуализация другой стороны пары показывает, что N рефлексивен как модуль над R при условии, что p — идеальная пара между M и N.

LaTeX

$$$\text{IsReflexive}(R,N)$, induced by $p$ via the right dual.$$

Lean4

@[deprecated Module.IsReflexive.of_isPerfPair (since := "2025-05-27")]
theorem reflexive_right : IsReflexive R N :=
  p.flip.reflexive_left

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