English
For a,b in the nonzero-divisors of M0, a divides b (in the submonoid of nonzero-divisors) iff a divides b when viewed in M0.
Русский
Для a,b ∈ M0⁰, a делит b в подмоноиде ненулевых делителей тогда и только тогда, когда a делит b в M0.
LaTeX
$$nonZeroDivisors_dvd_iff_dvd_coe {a b : M0⁰} : a ∣ b ↔ (a : M0) ∣ (b : M0)$$
Lean4
theorem nonZeroDivisors_dvd_iff_dvd_coe {a b : M₀⁰} : a ∣ b ↔ (a : M₀) ∣ (b : M₀) :=
⟨fun ⟨c, hc⟩ ↦ by simp_rw [hc, Submonoid.coe_mul, dvd_mul_right], fun ⟨c, hc⟩ ↦
⟨⟨c, (mul_mem_nonZeroDivisors.mp (hc ▸ b.prop)).2⟩, by simp_rw [Subtype.ext_iff, Submonoid.coe_mul, hc]⟩⟩