Zulip Chat Archive
Stream: general
Topic: Polymonial proof
Jiatong Gao (Apr 15 2025 at 01:16):
have h_Px : ∀ i : Fin 3, Polynomial.eval (x i) P = 54 := by
sorry
i want to ask how to prove this thing, I have no idea.
below is I defined
let P : Polynomial ℤ := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
let x : Fin 3 → ℤ := ![1, 2, 4]
Jiatong Gao (Apr 15 2025 at 01:23):
I tried to cases it
have h_Px : ∀ i : Fin 3, Polynomial.eval (x i) P = 54 := by
intro i
fin_cases i
· -- i = 0, x 0 = 1
simp [x, P, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
Polynomial.eval_X, Polynomial.eval_C]
norm_num
· -- i = 1, x 1 = 2
simp [x, P, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
Polynomial.eval_X, Polynomial.eval_C]
norm_num
· -- i = 2, x 2 = 4
simp [x, P, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
Polynomial.eval_X, Polynomial.eval_C]
norm_num
But failed, it says that
unsolved goals
case «0»
P : ℤ[X] := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
x : Fin 3 → ℤ := ![1, 2, 4]
y : Fin 2 → ℤ := ![0, 3]
h_x : ∀ (i j : Fin 3), i ≠ j → x i ≠ x j
h_y : ∀ (i j : Fin 2), i ≠ j → y i ≠ y j
⊢ False
Ilmārs Cīrulis (Apr 15 2025 at 01:32):
That's because the value of the polynomial in each case is 2013, not 54, probably?
import Mathlib
open Polynomial
noncomputable def P : Polynomial ℤ := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
def x : Fin 3 → ℤ := ![1, 2, 4]
theorem h_Px : ∀ i : Fin 3, Polynomial.eval (x i) P = 2013 := by
unfold P x
intro i
fin_cases i <;> simp
Jiatong Gao (Apr 15 2025 at 01:38):
Thanks a lot, there is full process now,I am the beginner and confused about how to figure there two polynomial out
import Mathlib
open Polynomial
/- Let $k$ and $n$ be positive integers and let $x_{1}, x_{2}, \ldots, x_{k}, y_{1}, y_{2}, \ldots, y_{n}$ be distinct integers. A polynomial $P$ with integer coefficients satisfies
$$
P\left(x_{1}\right)=P\left(x_{2}\right)=\ldots=P\left(x_{k}\right)=54
$$
and
$$
P\left(y_{1}\right)=P\left(y_{2}\right)=\ldots=P\left(y_{n}\right)=2013 .
$$
Determine the maximal value of $k n$. -/
theorem algebra_604776 :
∃ (k n : ℕ),
0 < k ∧ 0 < n ∧
∃ (x : Fin k → ℤ) (y : Fin n → ℤ),
(∀ i j : Fin k, i ≠ j → x i ≠ x j) ∧
(∀ i j : Fin n, i ≠ j → y i ≠ y j) ∧
∃ (P : Polynomial ℤ),
(∀ i, P.eval (x i) = 54) ∧
(∀ i, P.eval (y i) = 2013) ∧
k * n = 6 := by
let P : Polynomial ℤ := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
let x : Fin 3 → ℤ := ![1, 2, 4]
let y : Fin 2 → ℤ := ![0, 3]
have h_x : ∀ i j : Fin 3, i ≠ j → x i ≠ x j := by
intros i j hij
fin_cases i <;> fin_cases j
· contradiction
· dsimp [x]; decide
· dsimp [x]; decide
· dsimp [x]; decide
· contradiction
· dsimp [x]; decide
· dsimp [x]; decide
· dsimp [x]; decide
· contradiction
have h_y : ∀ i j : Fin 2, i ≠ j → y i ≠ y j := by
intros i j hij
fin_cases i <;> fin_cases j
· contradiction
· dsimp [y]; decide
· dsimp [y]; decide
· contradiction
have h_Px : ∀ i : Fin 3, Polynomial.eval (x i) P = 54 := by
sorry
have h_Py : ∀ i, Polynomial.eval (y i) P = 2013 := by
sorry
exact ⟨3, 2,
⟨by decide, by decide,
⟨x, y,
⟨h_x, h_y,
⟨P, ⟨h_Px, h_Py, by norm_num⟩⟩⟩⟩⟩⟩
Last updated: May 02 2025 at 03:31 UTC