instCancelMonoid — Mathlib

English

Let M and N be CancelMonoid. Then M × N is a CancelMonoid; in particular, right cancellation holds coordinatewise (and similarly left cancellation).

Русский

Пусть M и N — CancelMonoid. Тогда произведение M × N является CancelMonoid; в частности, отмена справа (а также слева) выполняется координатно.

LaTeX

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

Lean4

@[to_additive]
instance [CancelMonoid M] [CancelMonoid N] : CancelMonoid (M × N) :=
  { mul_right_cancel _ _ := by simp only [mul_left_inj, imp_self, forall_const] }

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