isLeftCancelMul — Mathlib

English

A submagma inherits left cancellation from a left cancellative magma: for all a,b,c in S, ab = ac implies b = c.

Русский

Подмагма наследует левое отменение от левоотменяющего magma: для всех a,b,c ∈ S, ab = ac ⇒ b = c.

LaTeX

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

Lean4

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

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