Skip to content

Fill polynomial evaluation norm step in Chapter 06#137

Open
heathsanchez wants to merge 1 commit into
mo271:mainfrom
heathsanchez:fix-chapter06-polynomial-eval-norm-step
Open

Fill polynomial evaluation norm step in Chapter 06#137
heathsanchez wants to merge 1 commit into
mo271:mainfrom
heathsanchez:fix-chapter06-polynomial-eval-norm-step

Conversation

@heathsanchez

Copy link
Copy Markdown

This replaces one local sorry in FormalBook/Chapter_06.lean inside a calculation in h_lamb_gt_q_sub_one.

The step simplifies evaluation of X - C lamb at (q : ℂ):

_ = ‖q - lamb‖^2 := by simp

Locally verified with:

lake build FormalBook.Chapter_06

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants