nonZeroDivisors_dvd_iff_dvd_coe — Mathlib

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]⟩⟩

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