isCancelMulZero — Mathlib

English

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

Русский

Подмножество подмагмы с нулём наследует отменяемость, если исходная магма отменяема с нулём.

LaTeX

$$$ \text{IsCancelMulZero}(s) \text{ (inherited from } IsCancelMulZero(M_0)\text{)} $$$

Lean4

/-- A submagma with zero of a cancellative magma with zero inherits cancellation. -/
instance isCancelMulZero [IsCancelMulZero M₀] : IsCancelMulZero s where

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