Repository navigation

Import monlib4 formalization - #76

Merged

Vilin97 merged 64 commits into

mainfrom

import/monlib4

Jun 1, 2026

Merged

Import monlib4 formalization#76
Vilin97 merged 64 commits into
mainfrom
import/monlib4

Commits on May 16, 2026
- Vendor monlib4 utility subset
  Vilin97
  committed
  8fddf55
Commits on May 18, 2026
- Merge branch 'main' into import/monlib4
  Vilin97
  authored
  29df37f
- Add monlib4 matrix automorphism theorem
  Vilin97
  committed
  8d78d48
- Fix monlib4 quality checks
  Vilin97
  committed
  4505114
- Add monlib4 theorem source
  Vilin97
  committed
  7edc297
- Trim unrelated monlib4 module
  Vilin97
  committed
  b608674
Commits on May 19, 2026
- Recover monlib4 quantum set core
  Vilin97
  committed
  73bb02f
- Add Monlib4 quantum graph core
  Vilin97
  committed
  3003a9a
- Add Monlib4 utility and inner-product modules
  Vilin97
  committed
  2da0703
- Merge origin/main into import/monlib4
  Vilin97
  committed
  1166b71
- Remove unrelated Monlib4 Sonia module
  Vilin97
  committed
  2e5673d
- Restore Monlib4 include block slice
  Vilin97
  committed
  9ed6f09
- Fix Monlib4 IncludeBlock warnings
  Vilin97
  committed
  dc73971
- Restore Monlib4 projection prerequisites
  Vilin97
  committed
  796775f
- Restore Monlib4 Ips operator lemmas
  Vilin97
  committed
  905e509
- Restore Monlib4 rank-one operators
  Vilin97
  committed
  7fce4d6
- Restore Monlib4 positive operator lemmas
  Vilin97
  committed
  40bc0f6
- Restore Monlib4 norm reconstruction lemmas
  Vilin97
  committed
  573dcc2
- Restore Monlib4 opposite-space helpers
  Vilin97
  committed
  63cb7ba
- Restore Monlib4 tensor equivalences
  Vilin97
  committed
  531c245
- Restore Monlib4 strict tensor and Sonia files
  Vilin97
  committed
  d01235f
- Restore Monlib4 bimodule multiplication maps
  Vilin97
  committed
  87734e4
- Restore Monlib4 quantum set delta form
  Vilin97
  committed
  8b4af21
- Restore Monlib4 Pi star ordered ring
  Vilin97
  committed
  3b10e10
- Restore Monlib4 Pi direct-sum tensor equivalence
  Vilin97
  committed
  08ca711
- Restore Monlib4 almost-Hermitian matrix spectra
  Vilin97
  committed
  230ffaf
- Restore Monlib4 complex norm preliminaries
  Vilin97
  committed
  865bacd
- Restore Monlib4 tensor Hilbert compatibility
  Vilin97
  committed
  866327e
- Restore Monlib4 algebra multiplication helpers
  Vilin97
  committed
  369e2a4
- Restore Monlib4 tensor-product orthonormal basis module
  Vilin97
  committed
  5eeec0f
- Restore Monlib4 quantum-set finite products
  Vilin97
  committed
  518c097
Commits on May 20, 2026
- Restore Monlib4 coalgebra layer
  Vilin97
  committed
  bae64bf
- Restore Monlib4 quantum-set identities
  Vilin97
  committed
  62aea78
- Restore Monlib4 star algebra equivalence API
  Vilin97
  committed
  34fabea
- Restore Monlib4 matrix basic lemmas
  Vilin97
  committed
  1627f76
- Restore Monlib4 tensor Hilbert tests
  Vilin97
  committed
  97c2cfa
- Restore Monlib4 Schur composition lemmas
  Vilin97
  committed
  1b5969d
- Restore Monlib4 inner automorphism cancellation lemmas
  Vilin97
  committed
  7826f0a
- Restore Monlib4 matrix automorphism support API
  Vilin97
  committed
  a8660e7
- Restore Monlib4 PiMat Fin two equivalences
  Vilin97
  committed
  27edd34
- Restore Monlib4 star algebra equivalence simp wrappers
  Vilin97
  committed
  36abd75
- Restore Monlib4 product automorphism API
  Vilin97
  committed
  8e5f574
- Restore Monlib4 matrix endomorphism equivalences
  Vilin97
  committed
  e3ab54a
- Restore Monlib4 tensor product star instance names
  Vilin97
  committed
  49f3b40
- Restore Monlib4 tensor product basic lemmas
  Vilin97
  committed
  c3c3f29
- Restore Monlib4 multiplicative opposite aliases
  Vilin97
  committed
  b50f47f
- Restore Monlib4 matrix basic identities
  Vilin97
  committed
  2538d82
- Restore Monlib4 tensor Hilbert instance aliases
  Vilin97
  committed
  4c80d71
- Restore Monlib4 matrix positivity compatibility
  Vilin97
  committed
  f8a00fe
- Restore Monlib4 matrix positivity aliases
  Vilin97
  committed
  865c879
- Restore Monlib4 matrix star order API
  Vilin97
  committed
  5e096e7
- Restore Monlib4 positive definite powers
  Vilin97
  committed
  d186445
- Restore Monlib4 quantum set inner algebra coherence
  Vilin97
  committed
  8970235
- Restore Monlib4 quantum set tensor product
  Vilin97
  committed
  b26571a
- Restore Monlib4 quantum set equivalence layer
  Vilin97
  committed
  c42567c
- Restore Monlib4 tensor submodule helpers
  Vilin97
  committed
  5d9b5e3
- Restore Monlib4 quantum set subset transport
  Vilin97
  committed
  e671d12
- Restore Monlib4 positive-map realness layer
  Vilin97
  committed
  39961d1
- Restore Monlib4 functional inner products
  Vilin97
  committed
  9439fbb
- Restore Monlib4 matrix inner products
  Vilin97
  committed
  d33520e
Commits on May 24, 2026
- Complete Monlib4 quantum graph import
  Vilin97
  committed
  9e835bb
- Merge remote-tracking branch 'origin/main' into import/monlib4
  Vilin97
  committed
  be9b1c7
- Complete monlib4 port
  Vilin97
  committed
  aca8a15
Commits on Jun 1, 2026
- Merge remote-tracking branch 'origin/main' into tmp-monlib4
  Vilin97
  committed
  0e975f8

Commits

Commits on May 16, 2026

Commits on May 18, 2026

Commits on May 19, 2026

Commits on May 20, 2026

Commits on May 24, 2026

Commits on Jun 1, 2026