English
DiophFn f and g imply that the function v ↦ f(v) % g(v) is Diophantine.
Русский
Если f и g — диофантовы функции, то функция v ↦ f(v) % g(v) диофантова.
LaTeX
$$$$\\forall \\{\\alpha : Type\\} {f,g:(\\alpha \\to \\mathbb{N})\\to \\mathbb{N},\\;\\mathrm{DiophFn}\\,f \\to \\mathrm{DiophFn}\\,g \\to \\mathrm{DiophFn}\\bigl(\\lambda v. f(v)\\%g(v)\\bigr).$$$$
Lean4
/-- Diophantine functions are closed under the modulo operation. -/
theorem mod_dioph : DiophFn fun v => f v % g v :=
have : Dioph fun v : Vector3 ℕ 3 => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x : ℕ, v &0 + v &2 * x = v &1 :=
(D&2 D= D.0 D∨ D&0 D< D&2) D∧ (D∃) 3 <| D&1 D+ D&3 D* D&0 D= D&2
diophFn_comp2 df dg <|
(diophFn_vec _).2 <|
ext this <|
(vectorAll_iff_forall _).1 fun z x y =>
show ((y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x) ↔ x % y = z from
⟨fun ⟨h, c, hc⟩ => by
rw [← hc]; simp only [add_mul_mod_self_left]; rcases h with x0 | hl
· rw [x0, mod_zero]
exact mod_eq_of_lt hl, fun e => by
rw [← e]
exact ⟨or_iff_not_imp_left.2 fun h => mod_lt _ (Nat.pos_of_ne_zero h), x / y, mod_add_div _ _⟩⟩
