finite_setOf_setGcd_dvd_and_mem_span

English

The set { n | setGcd(s) ∣ n ∧ n ∉ Ideal.span s } is finite.

Русский

Множество { n | gcd(s) ∣ n и n ∉ Ideal.span s } конечно по количеству.

LaTeX

$$$\\{ n \\mid \\mathrm{setGcd}(s) \\mid n \\ \\land\\ n \\notin \\mathrm{Ideal.span}(s) \\}.\\text{Finite}$$$

Lean4

theorem finite_setOf_setGcd_dvd_and_mem_span : {n | setGcd s ∣ n ∧ n ∉ Ideal.span s}.Finite :=
  have ⟨n, hn⟩ := exists_mem_closure_of_ge s
  (Finset.range n).finite_toSet.subset fun m h ↦
    Finset.mem_range.mpr <| lt_of_not_ge fun ge ↦ h.2 <| (Submodule.span_nat_eq_addSubmonoidClosure s).ge (hn m ge h.1)

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