eq_dioph — Mathlib

English

The set of places where two Diophantine functions are equal is Diophantine.

Русский

Множество мест, где две диагофантовые функции равны, диагофантово.

LaTeX

$$$$\mathrm{Dioph}(f) \land \mathrm{Dioph}(g) \Rightarrow \mathrm{Dioph}(\{v \mid f(v) = g(v)\})$$$$

Lean4

/-- The set of places where two Diophantine functions are equal is Diophantine. -/
theorem eq_dioph : Dioph fun v => f v = g v :=
  dioph_comp2 df dg <|
    of_no_dummies _ (Poly.proj &0 - Poly.proj &1) fun v => by
      exact Int.ofNat_inj.symm.trans ⟨@sub_eq_zero_of_eq ℤ _ (v &0) (v &1), eq_of_sub_eq_zero⟩

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