jstoobysmith
|
26e1fcb0bb
|
feat: Maxwell's equation
Also fix problem with derivatives.
|
2025-03-20 07:37:38 -04:00 |
|
Joseph Tooby-Smith
|
22cbaacbc5
|
Merge pull request #409 from HEPLean/Derivatives
feat: Coordinates in spacetime and derivatives
|
2025-03-20 06:58:58 -04:00 |
|
jstoobysmith
|
2c0b0b9a35
|
feat: Coordinates in spacetime and derivatives
|
2025-03-20 06:28:48 -04:00 |
|
Joseph Tooby-Smith
|
72219ab405
|
Merge pull request #408 from HEPLean/Derivatives
refactor: clean up redundent imports
|
2025-03-20 06:21:26 -04:00 |
|
jstoobysmith
|
64f7dfd74f
|
refactor: clean up redundent imports
|
2025-03-20 05:02:38 -04:00 |
|
Joseph Tooby-Smith
|
7b916e0b3c
|
Merge pull request #407 from HEPLean/Derivatives
feat: derivs of Real Lorentz tensors including field strength
|
2025-03-19 15:31:50 -04:00 |
|
jstoobysmith
|
b61203193f
|
refactor: Fix typo
Co-Authored-By: Matteo Cipollina <188064818+or4nge19@users.noreply.github.com>
|
2025-03-19 15:10:56 -04:00 |
|
jstoobysmith
|
df721e8c5c
|
refactor: Lint
|
2025-03-19 15:08:38 -04:00 |
|
jstoobysmith
|
7d773dca91
|
refactor: Lint
|
2025-03-19 14:55:29 -04:00 |
|
jstoobysmith
|
d06aa44162
|
feat: Prove of field strength derivative
|
2025-03-19 14:21:57 -04:00 |
|
jstoobysmith
|
63a00ffde5
|
Merge branch 'master' into Derivatives
|
2025-03-19 12:06:19 -04:00 |
|
Joseph Tooby-Smith
|
245401be33
|
Merge pull request #406 from HEPLean/Fix-TensorSpecies-Relation
feat: Tensor species move field
|
2025-03-19 12:04:01 -04:00 |
|
jstoobysmith
|
ba766e6c2f
|
feat: lemma for deriv_eq_deriv_on_coord
|
2025-03-19 12:01:19 -04:00 |
|
jstoobysmith
|
df399e31fa
|
Merge branch 'Fix-TensorSpecies-Relation' into Derivatives
|
2025-03-19 11:38:12 -04:00 |
|
Joseph Tooby-Smith
|
66b7b24c51
|
Merge pull request #405 from HEPLean/TwinParadox
feat: Twin paradox
|
2025-03-19 11:34:58 -04:00 |
|
jstoobysmith
|
329c50a721
|
refactor: Remove S.k
|
2025-03-19 11:28:27 -04:00 |
|
jstoobysmith
|
52f0e0058a
|
Merge branch 'TwinParadox' into Fix-TensorSpecies-Relation
|
2025-03-19 11:21:01 -04:00 |
|
jstoobysmith
|
6b17e73f62
|
feat: Add field to tensor species
|
2025-03-19 11:20:54 -04:00 |
|
jstoobysmith
|
6be3f23d1e
|
refactor: Lint
|
2025-03-19 11:00:45 -04:00 |
|
jstoobysmith
|
cec2719485
|
Update PhysLean.lean
|
2025-03-19 10:58:55 -04:00 |
|
jstoobysmith
|
844b3c272e
|
refactor: Typo
|
2025-03-19 10:56:03 -04:00 |
|
jstoobysmith
|
f33f8c3885
|
refactor: Lint
|
2025-03-19 10:55:11 -04:00 |
|
jstoobysmith
|
216f821c64
|
feat: Start at derivatives
|
2025-03-19 10:52:36 -04:00 |
|
jstoobysmith
|
bc8c2be21a
|
refactor: Free simps
|
2025-03-19 05:23:51 -04:00 |
|
Joseph Tooby-Smith
|
6375ee566c
|
Merge pull request #404 from HEPLean/Real-Lorentz-Tensors
feat: Proper time
|
2025-03-19 09:10:34 +00:00 |
|
jstoobysmith
|
dfbfda98ba
|
feat: Add Twin paradox
|
2025-03-18 18:09:27 +00:00 |
|
jstoobysmith
|
372089f6e0
|
refactor: Lint
|
2025-03-18 15:54:41 +00:00 |
|
jstoobysmith
|
742f895eab
|
feat: Add proper time
Co-Authored-By: Matteo Cipollina <188064818+or4nge19@users.noreply.github.com>
|
2025-03-18 15:49:34 +00:00 |
|
Joseph Tooby-Smith
|
922c3bf65b
|
Merge pull request #403 from HEPLean/Real-Lorentz-Tensors
feat: Invariance of causal character
|
2025-03-18 15:48:12 +00:00 |
|
jstoobysmith
|
e017d941da
|
refactor: Lint
|
2025-03-18 15:17:23 +00:00 |
|
jstoobysmith
|
b63d446bcc
|
feat: Invariance of causal character
Co-Authored-By: Matteo Cipollina <188064818+or4nge19@users.noreply.github.com>
|
2025-03-18 15:10:26 +00:00 |
|
Joseph Tooby-Smith
|
7b3896b44a
|
Merge pull request #402 from HEPLean/Real-Lorentz-Tensors
refactor: SpaceTime
|
2025-03-18 15:04:08 +00:00 |
|
jstoobysmith
|
34dd2ca45c
|
feat: Lint
|
2025-03-18 14:05:20 +00:00 |
|
jstoobysmith
|
1c085e97a9
|
refactor: Lint
|
2025-03-18 12:04:31 +00:00 |
|
jstoobysmith
|
e59a3137cd
|
refactor: SpaceTime
|
2025-03-18 11:59:24 +00:00 |
|
Joseph Tooby-Smith
|
dc13f3a7a9
|
Merge pull request #401 from HEPLean/Real-Lorentz-Tensors
feat: Causality for Lorentz vectors
|
2025-03-18 11:18:39 +00:00 |
|
jstoobysmith
|
27da280847
|
feat: Causality for Lorentz vectors
Co-Authored-By: Matteo Cipollina <188064818+or4nge19@users.noreply.github.com>
|
2025-03-18 10:59:00 +00:00 |
|
Joseph Tooby-Smith
|
f357262057
|
Merge pull request #400 from HEPLean/Real-Lorentz-Tensors
feat: Real Lorentz vectors
|
2025-03-18 10:46:25 +00:00 |
|
jstoobysmith
|
198d939c0d
|
refactor: Lint
|
2025-03-18 10:24:56 +00:00 |
|
jstoobysmith
|
7f5db45fa3
|
feat: Real Lorentz vectors
Co-Authored-By: Matteo Cipollina <188064818+or4nge19@users.noreply.github.com>
|
2025-03-18 09:50:34 +00:00 |
|
jstoobysmith
|
fc896722db
|
feat: Properties of Real tensors
|
2025-03-18 09:49:54 +00:00 |
|
jstoobysmith
|
c998f6d4ee
|
feat: Metrics for real Lorentz tensors
|
2025-03-18 05:54:57 +00:00 |
|
Joseph Tooby-Smith
|
6fb3c59837
|
Merge pull request #398 from HEPLean/Real-Lorentz-Tensors
feat: Field strength and derivative of tensors
|
2025-03-18 05:54:15 +00:00 |
|
jstoobysmith
|
92343aa56a
|
refactor: Lint
|
2025-03-18 05:32:24 +00:00 |
|
jstoobysmith
|
84e4985ba5
|
feat: Isomorphism
|
2025-03-18 05:18:55 +00:00 |
|
jstoobysmith
|
8f4dc2f7e2
|
feat: Field strength and derivative of tensors
|
2025-03-17 15:19:47 +00:00 |
|
Joseph Tooby-Smith
|
cb32040031
|
Merge pull request #397 from HEPLean/Real-Lorentz-Tensors
refactor: Field strength in Electromagnetism
|
2025-03-17 11:15:00 +00:00 |
|
jstoobysmith
|
0a1f7b3d3e
|
refactor: Fix build
|
2025-03-17 10:52:18 +00:00 |
|
jstoobysmith
|
e6a92e7b47
|
refactor: Field strength in Electromagnetism
|
2025-03-17 09:17:48 +00:00 |
|
Joseph Tooby-Smith
|
be3ccdae19
|
Merge pull request #396 from HEPLean/ClassicalMechanics
feat: Real Lorentz Tensors
|
2025-03-17 08:04:38 +00:00 |
|