instCovariantClassHSMulLe — Mathlib

English

The action by M on the lattice of ideals is compatible with the order, i.e., a CovariantClass instance holds for HSMul.

Русский

Действие M на решётке идеалов совместимо с порядком, существует экземпляр CovariantClass для HSMul.

LaTeX

$$$\text{CovariantClass } M\,(\text{Ideal } R)\;\text{instHSMul} $$$

Lean4

instance : CovariantClass M (Ideal R) HSMul.hSMul LE.le :=
  ⟨fun _ _ => map_mono⟩
    -- note: unlike with `Subring`, `mem_smul_pointwise_iff_exists` wouldn't be true

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