instIsLeftCancelMulLex — Mathlib

English

Lex α inherits left cancellation from α: if α has left cancellation for multiplication, then IsLeftCancelMul(Lex α) holds.

Русский

Лексическое расширение α наследует левую отменяемость умножения: если в α существует левое отменяющее свойство, то IsLeftCancelMul(Lex α) выполняется.

LaTeX

$$$ \forall \alpha\ [Mul\ \alpha]\ [IsLeftCancelMul\ \alpha],\ IsLeftCancelMul(\mathrm{Lex}\ \alpha). $$$

Lean4

@[to_additive]
instance [Mul α] [IsLeftCancelMul α] : IsLeftCancelMul (Lex α) :=
  inferInstanceAs <| IsLeftCancelMul α

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