noZeroDivisors — Mathlib

English

If α has NoZeroDivisors, then the nonnegative subtype { x ∈ α | 0 ≤ x } also has NoZeroDivisors.

Русский

Если α имеет нет нулевых делителей, то и подтип неотрицательных элементов обладает тем же свойством.

LaTeX

$$$\\text{NoZeroDivisors}\\, \\{ x : \\alpha \\mid 0 \\le x \\}$$$

Lean4

instance noZeroDivisors [Semiring α] [PartialOrder α] [IsOrderedRing α] [NoZeroDivisors α] :
    NoZeroDivisors { x : α // 0 ≤ x } :=
  {
    eq_zero_or_eq_zero_of_mul_eq_zero := by
      rintro ⟨a, ha⟩ ⟨b, hb⟩
      simp only [mk_mul_mk, mk_eq_zero, mul_eq_zero, imp_self] }

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