Finish the PolyType_0 lemma!

This commit is contained in:
chelseaandmadrid 2023-06-15 15:38:25 -07:00
parent 007e8cf795
commit 300007621a

View file

@ -198,6 +198,8 @@ lemma PolyType_0 (f : ) : (PolyType f 0) ↔ (∃ (c : ), ∃ (N :
have H22 := λ n=> (hh n).right have H22 := λ n=> (hh n).right
have H2 : c ≠ 0 := by have H2 : c ≠ 0 := by
exact H22 0 exact H22 0
have H2 : (c : ) ≠ 0 := by
simp; tauto
clear H22 clear H22
constructor constructor
· intro n Nn · intro n Nn
@ -206,47 +208,15 @@ lemma PolyType_0 (f : ) : (PolyType f 0) ↔ (∃ (c : ), ∃ (N :
tauto tauto
rw [this] rw [this]
have this2 : Polynomial.eval (n : ) Poly = (c : ) := by have this2 : Polynomial.eval (n : ) Poly = (c : ) := by
have this3 : ∀ r : , (Polynomial.eval r Poly) = (c : ) := (Poly_constant Poly (c : )).mp rfl have this3 : ∀ r : , (Polynomial.eval r Poly) = (c : ) := (Poly_constant Poly (c : )).mp rfl
exact this3 n exact this3 n
exact this2.symm exact this2.symm
· sorry · have this : Polynomial.degree Poly = 0 := by
-- intro n simp only [map_intCast]
-- specialize aaa n exact Polynomial.degree_C H2
-- have this1 : c ≠ 0 → f n = c := by tauto
-- sorry
-- rcases aaa with ⟨A, B⟩
-- have this1 : f n = c := by
-- tauto
-- constructor
-- clear A
-- · have this2 : ∀ (t : ), (Polynomial.eval t Poly) = (c : ) := by
-- rw [← Poly_constant Poly (c : )]
-- sorry
-- specialize this2 n
-- rw [this2]
-- tauto
-- · sorry
-- constructor
-- · intro n Nn
-- specialize aaa n
-- have this1 : c ≠ 0 → f n = c := by
-- tauto
-- rcases aaa with ⟨A, B⟩
-- have this1 : f n = c := by
-- tauto
-- clear A
-- have this2 : ∀ (t : ), (Polynomial.eval t Poly) = (c : ) := by
-- rw [← Poly_constant Poly (c : )]
-- sorry
-- specialize this2 n
-- rw [this2]
-- tauto
-- · sorry