instStarOrderedRing — Mathlib

English

The opposite ring R^op inherits a StarOrderedRing structure from R.

Русский

Противоположная окрестность кольца R^{op} наследует структуру StarOrderedRing от R.

LaTeX

$$StarOrderedRing(R^\mathrm{op})$$

Lean4

instance [NonUnitalSemiring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] : StarOrderedRing Rᵐᵒᵖ where
  le_iff x
    y :=
    by
    rw [← unop_le_unop, StarOrderedRing.le_iff, op_surjective.exists, ←
      (AddSubmonoid.closure _).comap_map_eq_of_injective opAddEquiv.injective]
    congr! with p
    ·
      simp [AddMonoidHom.map_mclosure, ← range_comp', Function.comp_def,
        ← (star_involutive.surjective.comp op_surjective).range_comp]
    · simp [← op_inj (α := R)]

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