English
Membership of the element constructed via Associates.mk a in the nonZeroDivisors of the Associates monoid is equivalent to a’s membership in the nonZeroDivisors of M.
Русский
Принадлежность элемента, полученного через Associates.mk a, к ненулевым делителям в левом моноиде Associates равна принадлежности a к ненулевым делителям в M.
LaTeX
$$mk_mem_nonZeroDivisors_associates : Associates.mk a ∈ (Associates M0)⁰ ↔ a ∈ M0⁰$$
Lean4
theorem mk_mem_nonZeroDivisors_associates : Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰ :=
by
rw [mem_nonZeroDivisors_iff_right, mem_nonZeroDivisors_iff_right, ← not_iff_not]
push_neg
constructor
· rintro ⟨⟨x⟩, hx₁, hx₂⟩
refine ⟨x, ?_, ?_⟩
· rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]
· rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]
· refine fun ⟨b, hb₁, hb₂⟩ ↦ ⟨Associates.mk b, ?_, by rwa [Associates.mk_ne_zero]⟩
rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]
