isCancelMul — Mathlib

English

If α is cancellative under addition, then the multiplicative version Multiplicative α is cancellative; i.e., for all a, b, c in α, a · b = a · c implies b = c.

Русский

Если α отменяем по сложению, то его копия в виде умножения, Multiplicative α, также обладает отменой по умножению; то есть для любых a, b, c ∈ α: a · b = a · c ⇒ b = c.

LaTeX

$$$[Add\,\alpha] \land [IsCancelAdd\,\alpha] \Rightarrow IsCancelMul(\text{Multiplicative }\alpha)$$$

Lean4

instance isCancelMul [Add α] [IsCancelAdd α] : IsCancelMul (Multiplicative α) :=
  ⟨⟩

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