SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-25 23:28:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Merge branch 'monalisa' of github.com:GTBarkley/comm_alg into monalisa

Browse source
This commit is contained in:
Andre 2023-06-16 17:42:17 -04:00
commit dd45702fca
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
CommAlg/final_poly_type.lean
View file

@ -5,6 +5,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
set_option maxHeartbeats 0
macro "ls" : tactic => `(tactic|library_search)
-- From Kyle : New tactic "obviously"
-- From Kyle : New tactic "obviously"
macro "obviously" : tactic =>
`(tactic| (
@ -79,9 +80,7 @@ lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) :
· sorry
-- Get the polynomial G (X) = F (X + s) from the polynomial F(X)
lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial ℚ), (∀ (x : ℚ),
Polynomial.eval x G = Polynomial.eval (x + s) F) ∧
(Polynomial.degree G = Polynomial.degree F) := by
lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by
sorry
-- Shifting doesn't change the polynomial type