Commit graph

  • f821bf71c5 edited README PfsProgs25 Dibyashanu Pati 2025-04-23 12:15:50 +05:30
  • 94802e942b attempt at the ideal gas law Dibyashanu Pati 2025-04-23 12:04:02 +05:30
  • 71a9b4fa49
    docs: Around classical harmonic oscillator. (#442) Joseph Tooby-Smith 2025-04-01 16:12:21 +00:00
  • f6739e9f31
    feat: Semiformal results around Em (#441) Joseph Tooby-Smith 2025-04-01 15:15:02 +00:00
  • dc5e8879de
    feat: Semi-formal results (#440) Joseph Tooby-Smith 2025-04-01 12:38:14 +00:00
  • 880bd44cb9
    feat: Sort TODOs better (#437) Joseph Tooby-Smith 2025-04-01 10:18:04 +00:00
  • 91d3f9388d
    Tagged TODOs (#435) Joseph Tooby-Smith 2025-04-01 08:15:18 +00:00
  • cac586d1bf
    feat: Add evaluation (#432) Joseph Tooby-Smith 2025-03-31 10:15:30 +00:00
  • a6a4a97011
    feat: Actions on tensors (#428) Joseph Tooby-Smith 2025-03-31 06:52:23 +00:00
  • f39411e5c9
    chore: Remove archive (#429) Joseph Tooby-Smith 2025-03-27 12:56:25 -04:00
  • 5925bfa16f
    General 1D Potential (#426) Ammar Husain 2025-03-26 15:34:57 -04:00
  • dbe181b002
    Merge pull request #427 from oeb25/master Joseph Tooby-Smith 2025-03-25 07:24:15 -04:00
  • cd5760ecc2 Update README links to new documentation location oeb25 2025-03-25 11:34:14 +01:00
  • d8df015c56
    Merge pull request #424 from HEPLean/erw Joseph Tooby-Smith 2025-03-24 13:36:55 -04:00
  • 1bbc9ac564 refactor: Lint jstoobysmith 2025-03-24 12:02:43 -04:00
  • 70ace79ccc feat: Remove more erws jstoobysmith 2025-03-24 11:50:41 -04:00
  • becf9d1841 chore: Remove mk_hom and mk_left from simp jstoobysmith 2025-03-24 10:44:48 -04:00
  • 0c9951d3b6 refactor: remove some erws jstoobysmith 2025-03-24 10:19:31 -04:00
  • d18ede024d chore: Replace Finset.sum_product jstoobysmith 2025-03-24 09:14:57 -04:00
  • c6d65bb308
    Merge pull request #423 from HEPLean/Tensors Joseph Tooby-Smith 2025-03-24 09:00:58 -04:00
  • 85a23a8fe4 refactor: Lint jstoobysmith 2025-03-24 07:40:28 -04:00
  • 35ebb44986 Update PhysLean.lean jstoobysmith 2025-03-24 07:15:40 -04:00
  • 24f2565bcb refactor: Lint jstoobysmith 2025-03-24 06:41:35 -04:00
  • f0a15e6068 feat: Defn TensorTreeQuot jstoobysmith 2025-03-24 06:28:05 -04:00
  • 34c300ccc7
    Merge pull request #422 from HEPLean/Tensors Joseph Tooby-Smith 2025-03-24 05:46:36 -04:00
  • 7f8f990570 Update MaxwellEquations.lean jstoobysmith 2025-03-24 05:19:13 -04:00
  • 0b41a58d83 chore: Lint & remove TODO jstoobysmith 2025-03-24 05:07:07 -04:00
  • dddbeb57d9
    Merge pull request #421 from placidex/todo Joseph Tooby-Smith 2025-03-23 16:02:03 -04:00
  • d0f3726cb5 Making the code more functional Krishna Padmasola 2025-03-23 23:06:24 +05:30
  • 93b955b28c
    Merge pull request #420 from HEPLean/style-lint-changes Joseph Tooby-Smith 2025-03-22 05:36:50 -04:00
  • 92b1266d70 feat: Lemmas regarding duals for real Lorentz tensors jstoobysmith 2025-03-21 14:56:48 -04:00
  • ad7ab11155
    Merge pull request #419 from HEPLean/style-lint-changes Joseph Tooby-Smith 2025-03-21 14:21:26 -04:00
  • cfcdb880c3 feat: Update todos jstoobysmith 2025-03-21 13:52:24 -04:00
  • acaf209961
    Merge pull request #418 from HEPLean/style-lint-changes Joseph Tooby-Smith 2025-03-21 12:32:11 -04:00
  • 7e5337ef0d Merge branch 'master' into style-lint-changes jstoobysmith 2025-03-21 11:39:15 -04:00
  • cebd21901f feat: Update bump.yml jstoobysmith 2025-03-21 11:39:09 -04:00
  • 73d2248671
    Merge pull request #417 from HEPLean/bump Joseph Tooby-Smith 2025-03-21 11:35:08 -04:00
  • b56c689121 feat: Update style lint jstoobysmith 2025-03-21 11:22:23 -04:00
  • 08f0a01e9d refactor: lint jstoobysmith 2025-03-21 11:12:58 -04:00
  • 1d7eeb7c4e feat: Boosts of Lorentz vectors jstoobysmith 2025-03-21 11:04:47 -04:00
  • 26897caaa5
    Merge pull request #416 from HEPLean/bump Joseph Tooby-Smith 2025-03-21 08:04:33 -04:00
  • 532e68e169 Update MaxwellEquations.lean jstoobysmith 2025-03-21 07:23:06 -04:00
  • d12947909d refactor: Lint jstoobysmith 2025-03-21 07:16:34 -04:00
  • 277538424a feat: Add ordinary boosts jstoobysmith 2025-03-21 07:11:42 -04:00
  • 04e14c389c
    Merge pull request #415 from HEPLean/bump Joseph Tooby-Smith 2025-03-20 13:23:41 -04:00
  • 812440c812 chore: Bump to v4.18.0-rc1 jstoobysmith 2025-03-20 12:56:28 -04:00
  • a662754b34
    Merge pull request #413 from HEPLean/bump-issue-template Joseph Tooby-Smith 2025-03-20 11:37:59 -04:00
  • 9f37aa5c8f feat: Create Bump.yml jstoobysmith 2025-03-20 11:15:56 -04:00
  • 666ac67a7e
    Merge pull request #410 from HEPLean/Derivatives Joseph Tooby-Smith 2025-03-20 09:37:56 -04:00
  • 869a9925ef refactor: lint jstoobysmith 2025-03-20 09:06:23 -04:00
  • 26e1fcb0bb feat: Maxwell's equation jstoobysmith 2025-03-20 07:37:38 -04:00
  • 22cbaacbc5
    Merge pull request #409 from HEPLean/Derivatives Joseph Tooby-Smith 2025-03-20 06:58:58 -04:00
  • 2c0b0b9a35 feat: Coordinates in spacetime and derivatives jstoobysmith 2025-03-20 06:28:48 -04:00
  • 72219ab405
    Merge pull request #408 from HEPLean/Derivatives Joseph Tooby-Smith 2025-03-20 06:21:26 -04:00
  • 64f7dfd74f refactor: clean up redundent imports jstoobysmith 2025-03-20 05:02:38 -04:00
  • 7b916e0b3c
    Merge pull request #407 from HEPLean/Derivatives Joseph Tooby-Smith 2025-03-19 15:31:50 -04:00
  • b61203193f refactor: Fix typo jstoobysmith 2025-03-19 15:10:56 -04:00
  • df721e8c5c refactor: Lint jstoobysmith 2025-03-19 15:08:38 -04:00
  • 7d773dca91 refactor: Lint jstoobysmith 2025-03-19 14:55:29 -04:00
  • d06aa44162 feat: Prove of field strength derivative jstoobysmith 2025-03-19 14:21:57 -04:00
  • 63a00ffde5 Merge branch 'master' into Derivatives jstoobysmith 2025-03-19 12:06:19 -04:00
  • 245401be33
    Merge pull request #406 from HEPLean/Fix-TensorSpecies-Relation Joseph Tooby-Smith 2025-03-19 12:04:01 -04:00
  • ba766e6c2f feat: lemma for deriv_eq_deriv_on_coord jstoobysmith 2025-03-19 12:01:19 -04:00
  • df399e31fa Merge branch 'Fix-TensorSpecies-Relation' into Derivatives jstoobysmith 2025-03-19 11:38:12 -04:00
  • 66b7b24c51
    Merge pull request #405 from HEPLean/TwinParadox Joseph Tooby-Smith 2025-03-19 11:34:58 -04:00
  • 329c50a721 refactor: Remove S.k jstoobysmith 2025-03-19 11:28:27 -04:00
  • 52f0e0058a Merge branch 'TwinParadox' into Fix-TensorSpecies-Relation jstoobysmith 2025-03-19 11:21:01 -04:00
  • 6b17e73f62 feat: Add field to tensor species jstoobysmith 2025-03-19 11:20:54 -04:00
  • 6be3f23d1e refactor: Lint jstoobysmith 2025-03-19 11:00:45 -04:00
  • cec2719485 Update PhysLean.lean jstoobysmith 2025-03-19 10:58:55 -04:00
  • 844b3c272e refactor: Typo jstoobysmith 2025-03-19 10:56:03 -04:00
  • f33f8c3885 refactor: Lint jstoobysmith 2025-03-19 10:55:11 -04:00
  • 216f821c64 feat: Start at derivatives jstoobysmith 2025-03-19 10:52:36 -04:00
  • bc8c2be21a refactor: Free simps jstoobysmith 2025-03-19 05:23:51 -04:00
  • 6375ee566c
    Merge pull request #404 from HEPLean/Real-Lorentz-Tensors Joseph Tooby-Smith 2025-03-19 09:10:34 +00:00
  • dfbfda98ba feat: Add Twin paradox jstoobysmith 2025-03-18 18:09:27 +00:00
  • 372089f6e0 refactor: Lint jstoobysmith 2025-03-18 15:54:41 +00:00
  • 742f895eab feat: Add proper time jstoobysmith 2025-03-18 15:49:34 +00:00
  • 922c3bf65b
    Merge pull request #403 from HEPLean/Real-Lorentz-Tensors Joseph Tooby-Smith 2025-03-18 15:48:12 +00:00
  • e017d941da refactor: Lint jstoobysmith 2025-03-18 15:17:23 +00:00
  • b63d446bcc feat: Invariance of causal character jstoobysmith 2025-03-18 15:10:26 +00:00
  • 7b3896b44a
    Merge pull request #402 from HEPLean/Real-Lorentz-Tensors Joseph Tooby-Smith 2025-03-18 15:04:08 +00:00
  • 34dd2ca45c feat: Lint jstoobysmith 2025-03-18 14:05:20 +00:00
  • 1c085e97a9 refactor: Lint jstoobysmith 2025-03-18 12:04:31 +00:00
  • e59a3137cd refactor: SpaceTime jstoobysmith 2025-03-18 11:59:24 +00:00
  • dc13f3a7a9
    Merge pull request #401 from HEPLean/Real-Lorentz-Tensors Joseph Tooby-Smith 2025-03-18 11:18:39 +00:00
  • 27da280847 feat: Causality for Lorentz vectors jstoobysmith 2025-03-18 10:59:00 +00:00
  • f357262057
    Merge pull request #400 from HEPLean/Real-Lorentz-Tensors Joseph Tooby-Smith 2025-03-18 10:46:25 +00:00
  • 198d939c0d refactor: Lint jstoobysmith 2025-03-18 10:24:56 +00:00
  • 7f5db45fa3 feat: Real Lorentz vectors jstoobysmith 2025-03-18 09:50:34 +00:00
  • fc896722db feat: Properties of Real tensors jstoobysmith 2025-03-18 09:49:54 +00:00
  • c998f6d4ee feat: Metrics for real Lorentz tensors jstoobysmith 2025-03-18 05:54:57 +00:00
  • 6fb3c59837
    Merge pull request #398 from HEPLean/Real-Lorentz-Tensors Joseph Tooby-Smith 2025-03-18 05:54:15 +00:00
  • 92343aa56a refactor: Lint jstoobysmith 2025-03-18 05:32:24 +00:00
  • 84e4985ba5 feat: Isomorphism jstoobysmith 2025-03-18 05:18:55 +00:00
  • 8f4dc2f7e2 feat: Field strength and derivative of tensors jstoobysmith 2025-03-17 15:19:47 +00:00
  • cb32040031
    Merge pull request #397 from HEPLean/Real-Lorentz-Tensors Joseph Tooby-Smith 2025-03-17 11:15:00 +00:00
  • 0a1f7b3d3e refactor: Fix build jstoobysmith 2025-03-17 10:52:18 +00:00
  • e6a92e7b47 refactor: Field strength in Electromagnetism jstoobysmith 2025-03-17 09:17:48 +00:00
  • be3ccdae19
    Merge pull request #396 from HEPLean/ClassicalMechanics Joseph Tooby-Smith 2025-03-17 08:04:38 +00:00