mul_dioph

Mathlib.NumberTheory.Dioph

URI: https://scilib.ai/kg/mathlib#Dioph.mul_dioph

← MathLib Explorer

English

Diophantine functions are closed under multiplication.

Русский

Диофантовы функции замыкаются по умножению.

LaTeX

$$$$\mathrm{DiophFn}(f) \Rightarrow \mathrm{DiophFn}(g) \Rightarrow \mathrm{DiophFn}(f \cdot g)$$$$

Lean4

/-- Diophantine functions are closed under multiplication. -/
theorem mul_dioph : DiophFn fun v => f v * g v :=
  diophFn_comp2 df dg <| abs_poly_dioph (@Poly.proj (Fin2 2) &0 * @Poly.proj (Fin2 2) &1)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru