instIsOrderedMonoidValueGroupWithZero

English

The structure ValueGroupWithZero R forms an ordered monoid: multiplication preserves the order from the left. If a ≤ b then c a ≤ c b for all c.

Русский

Структура ValueGroupWithZero R образует упорядоченный моноид: умножение слева сохраняет порядок. Если a ≤ b, то для любого c выполняется c a ≤ c b.

LaTeX

$$$\forall a,b,c \,(a \le b) \Rightarrow (c a \le c b) \quad \text{in } \mathrm{ValueGroupWithZero}(R)$$$

Lean4

instance : IsOrderedMonoid (ValueGroupWithZero R) where
  mul_le_mul_left a b hab
    c := by
    induction a using ValueGroupWithZero.ind
    induction b using ValueGroupWithZero.ind
    induction c using ValueGroupWithZero.ind
    simp only [ValueGroupWithZero.mk_mul_mk, ValueGroupWithZero.mk_le_mk, Submonoid.coe_mul]
    conv_lhs => apply mul_mul_mul_comm
    conv_rhs => apply mul_mul_mul_comm
    apply rel_mul_left
    exact hab

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