feat: Add first EvalT and ProdT Interaction Lemma - #1344
Conversation
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
jstoobysmith
added
awaiting-author
| lemma evalT_prodT_right {n n1 : ℕ} {c : Fin n → C} {c1 : Fin (n1 + 1) → C} | ||
| (i : Fin (n1 + 1)) (x : basisIdx (c1 i)) (t : Tensor S c) (t1 : Tensor S c1) : | ||
| permT id (IsReindexing.append_succAbove_natAdd (n := n) (n1 := n1) i) | ||
| (evalT (Fin.natAdd (m := n1 + 1) n i) (basisIdxCongr (by simp) x) (prodT t t1)) = |
There was a problem hiding this comment.
I would swap the equality around so that what is currently on the RHS is now on the LHS.
| permT id (IsReindexing.append_succAbove_natAdd (n := n) (n1 := n1) i) | ||
| (evalT (Fin.natAdd (m := n1 + 1) n i) (basisIdxCongr (by simp) x) (prodT t t1)) = | ||
| prodT t (evalT i x t1) := by | ||
| apply Tensor.induction_on_basis (t := t) |
There was a problem hiding this comment.
If you search for induction_on_basis in Physlib you will see a better way of doing this using induction' t with ....
jstoobysmith
added
the
awaiting-author
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
|
Hi @jstoobysmith eventually it's green |
|
Hey @NicolaBernini would you mind commenting with when done with a PR :) - I use a filter based on this label to determine what PRs to look at. |
github-actions
Bot
removed
the
awaiting-author
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Looks good though - approved.
jstoobysmith
added
the
ready-to-merge
2 participants
Overview
Add first EvalT and ProdT Interaction Lemma