Submagmas with zero inherit cancellations

instance MulZeroMemClass.isLeftCancelMulZero {M₀ : Type u_1} [Mul M₀] [Zero M₀] {S : Type u_2} [SetLike S M₀] [MulMemClass S M₀] [ZeroMemClass S M₀] (s : S) [IsLeftCancelMulZero M₀] : IsLeftCancelMulZero ↥s

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

instance MulZeroMemClass.isRightCancelMulZero {M₀ : Type u_1} [Mul M₀] [Zero M₀] {S : Type u_2} [SetLike S M₀] [MulMemClass S M₀] [ZeroMemClass S M₀] (s : S) [IsRightCancelMulZero M₀] : IsRightCancelMulZero ↥s

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

instance MulZeroMemClass.isCancelMulZero {M₀ : Type u_1} [Mul M₀] [Zero M₀] {S : Type u_2} [SetLike S M₀] [MulMemClass S M₀] [ZeroMemClass S M₀] (s : S) [IsCancelMulZero M₀] : IsCancelMulZero ↥s

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