refactor: Weyl fermions#1360
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 |
nateabr
left a comment
nateabr
left a comment
There was a problem hiding this comment.
Hi I went through this, very very minor comments but apart from that looks great.
| - fromPairT (DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0) := by | ||
| rw [dualRightMetric_eq_fromPairT, dualRightMetricVal_expand_tmul] | ||
| simp | ||
|
|
There was a problem hiding this comment.
A little unsure about this but the names for the lemma's you've provided above, wont having the declaration as you've written with a dot (eg. dualRightMetric_eq_DualRightHandedWeyl.basis ) automatically register the prefix as namespace within this environment?
Was this your intention? Might be better to use an underscore if not?
| ∑ i, fromPairT (RightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis i) := by | ||
| rw [rightDualRightUnit_eq_fromPairT, rightDualRightUnitVal_expand_tmul] | ||
| rfl | ||
|
|
There was a problem hiding this comment.
Same issue as my prior comment.
2 participants
Refactoring Weyl fermions. All of the changes with content take place in ../Weyl/Basic.lean (and one or two changes in ../Weyl/Module.lean). Everything downstream of that is just fixing what broke.
Idea here is to improve the naming around Weyl fermions, and to improve the structure of the API.