isLeftCancelMulZero — Mathlib

English

A submagma with zero of a left cancellative magma with zero inherits left cancellation.

Русский

Подмножество подмагмы с нулём внутри левого отменяющего magma c нулём наследует левую отменяемость.

LaTeX

$$$ \text{If } M_0 \text{ is left-cancellative with zero, then } s \text{ inherits left cancellation.} $$$

Lean4

/-- A submagma with zero of a left cancellative magma with zero inherits left cancellation. -/
instance isLeftCancelMulZero [IsLeftCancelMulZero M₀] : IsLeftCancelMulZero s :=
  Subtype.coe_injective.isLeftCancelMulZero Subtype.val rfl fun _ _ => rfl

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