instCancelCommMonoid — Mathlib

English

If M and N are CancelCommMonoid, then M × N is a CancelCommMonoid; in particular, both left and right cancellation hold in the product.

Русский

Если M и N — CancelCommMonoid, то M × N является CancelCommMonoid; в произведении выполняются и слева, и справа отмены.

LaTeX

$$$\mathrm{CancelCommMonoid}(M) \wedge \mathrm{CancelCommMonoid}(N) \implies \mathrm{CancelCommMonoid}(M \times N)$$$

Lean4

@[to_additive]
instance [CancelCommMonoid M] [CancelCommMonoid N] : CancelCommMonoid (M × N) :=
  { mul_left_cancel _ _ := by simp }

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