English
If α has no zero divisors, then WithTop α also has no zero divisors; i.e., if a·b = 0 in WithTop α, then either a = 0 or b = 0.
Русский
Если вα нет нулевых делителей, то и в WithTop α нет нулевых делителей; то есть если a·b = 0 в WithTop α, то либо a = 0, либо b = 0.
LaTeX
$$$\\\\forall a,b \\in \\mathrm{WithTop}\\\\,\\\\alpha, a \\cdot b = 0 \\\\Rightarrow a = 0 \\\\lor b = 0$$$
Lean4
instance instNoZeroDivisors [NoZeroDivisors α] : NoZeroDivisors (WithTop α) :=
by
refine ⟨fun h₁ => Decidable.byContradiction fun h₂ => ?_⟩
rw [mul_def, if_neg h₂] at h₁
rcases Option.mem_map₂_iff.1 h₁ with ⟨a, b, (rfl : _ = _), (rfl : _ = _), hab⟩
exact h₂ ((eq_zero_or_eq_zero_of_mul_eq_zero hab).imp (congr_arg some) (congr_arg some))
