fintypeSubtypeDvd — Mathlib

English

If y is nonzero in a unique factorization monoid with finitely many units, then the set of divisors of y is finite; more precisely, {x | x ∣ y} is a finite type.

Русский

Если y ≠ 0 в уникализационном моноиде с конечным числом единиц, то множество делителей y конечное.

LaTeX

$$$\\text{Fintype }\\{x\\,|\\, x \\mid y\\}\\quad\\text{for } y \\neq 0$$$

Lean4

/-- If `y` is a nonzero element of a unique factorization monoid with finitely
many units (e.g. `ℤ`, `Ideal (ring_of_integers K)`), it has finitely many divisors. -/
noncomputable def fintypeSubtypeDvd {M : Type*} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [Fintype Mˣ]
    (y : M) (hy : y ≠ 0) : Fintype { x // x ∣ y } :=
  by
  haveI : Nontrivial M := ⟨⟨y, 0, hy⟩⟩
  haveI : NormalizationMonoid M := UniqueFactorizationMonoid.normalizationMonoid
  haveI := Classical.decEq M
  haveI :=
    Classical.decEq
      (Associates M)
        -- We'll show `fun (u : Mˣ) (f ⊆ factors y) ↦ u * Π f` is injective
          -- and has image exactly the divisors of `y`.

  refine
    Fintype.ofFinset
      (((normalizedFactors y).powerset.toFinset ×ˢ (Finset.univ : Finset Mˣ)).image fun s => (s.snd : M) * s.fst.prod)
      fun x => ?_
  simp only [Finset.mem_image, Finset.mem_product, Finset.mem_univ, and_true, Multiset.mem_toFinset,
    Multiset.mem_powerset]
  constructor
  · rintro ⟨s, hs, rfl⟩
    change (s.snd : M) * s.fst.prod ∣ y
    rw [(unit_associated_one.mul_right s.fst.prod).dvd_iff_dvd_left, one_mul, ←
      (prod_normalizedFactors hy).dvd_iff_dvd_right]
    exact Multiset.prod_dvd_prod_of_le hs
  · rintro (h : x ∣ y)
    have hx : x ≠ 0 := by
      refine mt (fun hx => ?_) hy
      rwa [hx, zero_dvd_iff] at h
    obtain ⟨u, hu⟩ := prod_normalizedFactors hx
    refine ⟨⟨normalizedFactors x, u⟩, ?_, (mul_comm _ _).trans hu⟩
    exact (dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mp h

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