Revision #1516 → #1784 · back to history
modifiedAddition and multiplication of amplitude arrowsb76a7af3e44c
| Field | From #1516 | To #1784 |
|---|
| mathlib.match_kind | — | generalization |
| mathlib.module | Mathlib.Analysis.Normed.Field.Basic | Mathlib.Analysis.Normed.Ring.Basic |
| note | Amplitude arrows are complex numbers and their multiplicative-length rule is the verified multiplicativity of norm (`norm_mul`), but the physics framing is not formalized. | Amplitude arrows are complex numbers whose multiplicative-length rule is the verified multiplicativity of norm (`norm_mul` in `Mathlib.Analysis.Normed.Ring.Basic`), but the physics framing is not formalized. |
modifiedQED as abelian gauge theory U(1)bd81a51f87f2
| Field | From #1516 | To #1784 |
|---|
| mathlib.match_kind | — | generalization |
modifiedDirac spinor field2f597c8b8461
| Field | From #1516 | To #1784 |
|---|
| note | No spinor or spinor-field definitions exist in Mathlib. | No spinor or spinor-field definitions exist in Mathlib (case-insensitive grep for `spinor` returned no files). |
modifiedDyson's argument: zero radius of convergence14290bd3d08c
| Field | From #1516 | To #1784 |
|---|
| mathlib.match_kind | — | generalization |
addedAsymptotic series93a357e2d28c
addedLorenz gauge condition0437c0d86c6c
addedTime-ordering operatorfc57b51ed517
addedWave operator (d'Alembertian)1b11dbf735b9
addedMinkowski space (flat spacetime)8a95260ae597