isRightCancelMul — Mathlib

English

A submagma inherits right cancellation: for all a,b,c in S, ab = cb implies a = c.

Русский

Подмагма наследует правое отменение: для всех a,b,c ∈ S, ab = cb ⇒ a = c.

LaTeX

$$$ \forall a,b,c \in S, a b = c b \\Rightarrow a = c $$$

Lean4

/-- A submagma of a right cancellative magma inherits right cancellation. -/
@[to_additive /-- An additive submagma of a right cancellative additive magma inherits right cancellation. -/
    ]
instance isRightCancelMul [IsRightCancelMul M] (S : A) : IsRightCancelMul S :=
  Subtype.coe_injective.isRightCancelMul Subtype.val fun _ _ => rfl

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