Skip to content

feat: AddTorsor instance on space #972

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jstoobysmith merged 7 commits into from
Mar 7, 2026
+685 −564
Merged

feat: AddTorsor instance on space #972

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
03cbedb
feat: AddTorsor instance on space
jstoobysmith Mar 5, 2026
761c652
refactor: Redefine VSub
jstoobysmith Mar 5, 2026
ebccb6d
refactor: Split basic and module
jstoobysmith Mar 5, 2026
a8da782
refactor: Fix spelling
jstoobysmith Mar 5, 2026
2a4c47b
feat: Fix def-eq abuse
jstoobysmith Mar 6, 2026
006122f
Merge branch 'master' into SpaceAddTorsor
jstoobysmith Mar 6, 2026
8f236b2
feat: Add structure of manifold
jstoobysmith Mar 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions PhysLean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -352,6 +352,7 @@ import PhysLean.SpaceAndTime.Space.Integrals.Basic
import PhysLean.SpaceAndTime.Space.Integrals.RadialAngularMeasure
import PhysLean.SpaceAndTime.Space.IsDistBounded
import PhysLean.SpaceAndTime.Space.LengthUnit
import PhysLean.SpaceAndTime.Space.Module
import PhysLean.SpaceAndTime.Space.Norm
import PhysLean.SpaceAndTime.Space.Slice
import PhysLean.SpaceAndTime.Space.Translations
Expand Down
2 changes: 1 addition & 1 deletion PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Gregory J. Loges
-/
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.MeasureTheory.Function.L2Space
import PhysLean.SpaceAndTime.Space.Basic
import PhysLean.SpaceAndTime.Space.Module
/-!

# Hilbert space for quantum mechanics on Space d
Expand Down
Loading