instNoZeroDivisors — Mathlib

English

If α has no zero divisors, then WithBot α also has no zero divisors. The property passes from α to the bottom-extended structure.

Русский

Если у α нет нулевых делителей, то и WithBot α также не имеет нулевых делителей. Это свойство переносится из α в расширение снизу.

LaTeX

$$$\text{NoZeroDivisors}(α) \Rightarrow \text{NoZeroDivisors}(WithBot α)$$$

Lean4

instance instNoZeroDivisors [NoZeroDivisors α] : NoZeroDivisors (WithBot α) :=
  WithTop.instNoZeroDivisors

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