Import monlib4 formalization

LeanPool.lean

@@ -386,6 +386,104 @@ import LeanPool.LowDimSolvClassification.LemmasDim3
 import LeanPool.LowDimSolvClassification.QuotientSolvable
 import LeanPool.LowDimSolvClassification.Semidirect
 import LeanPool.LowDimSolvClassification.Tactics
+import LeanPool.Monlib4
+import LeanPool.Monlib4.LinearAlgebra
+import LeanPool.Monlib4.LinearAlgebra.Coalgebra
+import LeanPool.Monlib4.LinearAlgebra.Coalgebra.FiniteDimensional
+import LeanPool.Monlib4.LinearAlgebra.Coalgebra.Lemmas
+import LeanPool.Monlib4.LinearAlgebra.Coalgebra.MulOpposite
+import LeanPool.Monlib4.LinearAlgebra.DirectSumFromTo
+import LeanPool.Monlib4.LinearAlgebra.End
+import LeanPool.Monlib4.LinearAlgebra.InnerAut
+import LeanPool.Monlib4.LinearAlgebra.InvariantSubmodule
+import LeanPool.Monlib4.LinearAlgebra.Ips
+import LeanPool.Monlib4.LinearAlgebra.Ips.Basic
+import LeanPool.Monlib4.LinearAlgebra.Ips.Frob
+import LeanPool.Monlib4.LinearAlgebra.Ips.Functional
+import LeanPool.Monlib4.LinearAlgebra.Ips.Ips
+import LeanPool.Monlib4.LinearAlgebra.Ips.MatIps
+import LeanPool.Monlib4.LinearAlgebra.Ips.MinimalProj
+import LeanPool.Monlib4.LinearAlgebra.Ips.MulOp
+import LeanPool.Monlib4.LinearAlgebra.Ips.Nontracial
+import LeanPool.Monlib4.LinearAlgebra.Ips.OpUnop
+import LeanPool.Monlib4.LinearAlgebra.Ips.Pos
+import LeanPool.Monlib4.LinearAlgebra.Ips.RankOne
+import LeanPool.Monlib4.LinearAlgebra.Ips.Strict
+import LeanPool.Monlib4.LinearAlgebra.Ips.Symm
+import LeanPool.Monlib4.LinearAlgebra.Ips.TensorHilbert
+import LeanPool.Monlib4.LinearAlgebra.Ips.Vn
+import LeanPool.Monlib4.LinearAlgebra.IsProj'
+import LeanPool.Monlib4.LinearAlgebra.IsReal
+import LeanPool.Monlib4.LinearAlgebra.KroneckerToTensor
+import LeanPool.Monlib4.LinearAlgebra.LinearMapOp
+import LeanPool.Monlib4.LinearAlgebra.LmulRmul
+import LeanPool.Monlib4.LinearAlgebra.Matrix
+import LeanPool.Monlib4.LinearAlgebra.Matrix.Basic
+import LeanPool.Monlib4.LinearAlgebra.Matrix.Cast
+import LeanPool.Monlib4.LinearAlgebra.Matrix.Conj
+import LeanPool.Monlib4.LinearAlgebra.Matrix.IncludeBlock
+import LeanPool.Monlib4.LinearAlgebra.Matrix.IsAlmostHermitian
+import LeanPool.Monlib4.LinearAlgebra.Matrix.PiMat
+import LeanPool.Monlib4.LinearAlgebra.Matrix.PosDefRpow
+import LeanPool.Monlib4.LinearAlgebra.Matrix.PosEqLinearMapIsPositive
+import LeanPool.Monlib4.LinearAlgebra.Matrix.Reshape
+import LeanPool.Monlib4.LinearAlgebra.Matrix.Spectra
+import LeanPool.Monlib4.LinearAlgebra.Matrix.StarOrderedRing
+import LeanPool.Monlib4.LinearAlgebra.Mul''
+import LeanPool.Monlib4.LinearAlgebra.MyBimodule
+import LeanPool.Monlib4.LinearAlgebra.MySpec
+import LeanPool.Monlib4.LinearAlgebra.Nacgor
+import LeanPool.Monlib4.LinearAlgebra.OfNorm
+import LeanPool.Monlib4.LinearAlgebra.PiDirectSum
+import LeanPool.Monlib4.LinearAlgebra.PiStarOrderedRing
+import LeanPool.Monlib4.LinearAlgebra.PosMapIsReal
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.Basic
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.DeltaForm
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.Instances
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.PhiMap
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.Pi
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.QIso
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.SchurMul
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.SchurMulTensor
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.Subset
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.Symm
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet.TensorProduct
+import LeanPool.Monlib4.LinearAlgebra.TensorProduct
+import LeanPool.Monlib4.LinearAlgebra.TensorProduct.BasicLemmas
+import LeanPool.Monlib4.LinearAlgebra.TensorProduct.FiniteDimensional
+import LeanPool.Monlib4.LinearAlgebra.TensorProduct.Lemmas
+import LeanPool.Monlib4.LinearAlgebra.TensorProduct.OrthonormalBasis
+import LeanPool.Monlib4.LinearAlgebra.TensorProduct.Submodule
+import LeanPool.Monlib4.LinearAlgebra.ToMatrixOfEquiv
+import LeanPool.Monlib4.Monlib
+import LeanPool.Monlib4.Other
+import LeanPool.Monlib4.Other.Sonia
+import LeanPool.Monlib4.Preq
+import LeanPool.Monlib4.Preq.Complex
+import LeanPool.Monlib4.Preq.Dite
+import LeanPool.Monlib4.Preq.Equiv
+import LeanPool.Monlib4.Preq.Finset
+import LeanPool.Monlib4.Preq.Ites
+import LeanPool.Monlib4.Preq.RCLikeLe
+import LeanPool.Monlib4.Preq.Set
+import LeanPool.Monlib4.Preq.StarAlgEquiv
+import LeanPool.Monlib4.QuantumGraph
+import LeanPool.Monlib4.QuantumGraph.Basic
+import LeanPool.Monlib4.QuantumGraph.Degree
+import LeanPool.Monlib4.QuantumGraph.Example
+import LeanPool.Monlib4.QuantumGraph.Grad
+import LeanPool.Monlib4.QuantumGraph.Iso
+import LeanPool.Monlib4.QuantumGraph.Matrix
+import LeanPool.Monlib4.QuantumGraph.Nontracial
+import LeanPool.Monlib4.QuantumGraph.OfClassicalGraph
+import LeanPool.Monlib4.QuantumGraph.PiMat
+import LeanPool.Monlib4.QuantumGraph.PiMatFinTwo
+import LeanPool.Monlib4.QuantumGraph.QamA
+import LeanPool.Monlib4.QuantumGraph.QamAExample
+import LeanPool.Monlib4.QuantumGraph.ToProjections
+import LeanPool.Monlib4.RepTheory
+import LeanPool.Monlib4.RepTheory.AutMat
 import LeanPool.Monsky
 import LeanPool.Monsky.Appendix
 import LeanPool.Monsky.BasicDefinitions

LeanPool/Monlib4.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 Monica Omar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Monica Omar
+-/
+
+import LeanPool.Monlib4.Monlib
+
+/-!
+# Monlib4 Operator-Algebra and Quantum-Set Core
+
+Source: doi:10.4169/amer.math.monthly.124.10.966
+Authors: Monica Omar
+Status: verified
+Main declarations: `Matrix.aut_mat_inner`, `QuantumSet`, `schurMul`, `QuantumGraph`
+Tags: linear-algebra, operator-algebras, quantum-sets, quantum-graphs, representation-theory
+MSC: 15A69, 16W20
+-/
+
+/-!
+## Mathematical overview
+
+A theorem-bearing subset of `monlib4` — a Lean 4 formalization of
+non-commutative graph theory. The upstream library builds quantum-graph and
+quantum-set theory on substantial matrix / inner-product-space infrastructure.
+
+This vendored subset includes the upstream matrix-algebra automorphism theorem:
+every automorphism of a finite matrix algebra over a field is inner, implemented
+by conjugation with an invertible matrix (`Matrix.aut_mat_inner` and
+`Matrix.aut_mat_inner'`). As a corollary, such automorphisms preserve trace
+(`Matrix.aut_mat_inner_trace_preserving`).
+
+The recovered downstream operator-algebra layer adds unitary inner
+star-algebra automorphisms (`unitary.innerAutStarAlg`), their matrix
+specialization as linear maps (`Matrix.innerAut`), and preservation results for
+trace, spectrum, multiplication, star, inverses, and Hermitian matrices.  The
+quantum-set core now includes `starAlgebra`, `InnerProductAlgebra`,
+`QuantumSet`, the modular-automorphism identities, the complex quantum set
+instance `Complex.quantumSet`, finite product quantum sets, delta-form quantum
+sets, and the star-preserving map API `LinearMap.IsReal` / `LinearMap.real`.
+The recovered quantum-graph core includes the Schur product `schurMul`, Schur
+projections, and the predicates `QuantumGraph` / `QuantumGraph.Real`.
+
+The supporting imported infrastructure also includes a `Matrix.reshape` linear
+equivalence between `Mₙₓₘ(R)` and `Rⁿˣᵐ`, the entrywise conjugate `Matrix.conj`
+with the `ᴴᵀ` notation, the projection `directSumFromTo` between summands of a
+dependent direct sum, basic spectrum commutativity (`isUnit_comm`,
+`spectrum.comm`), the `PiMat` matrix-family abbreviation, permutation-matrix
+unitarity, self-adjoint/inner-product extensionality lemmas, strict
+tensor-product coercions, left/right multiplication maps and bimodule maps on
+tensor products, the finite-dimensional Hilbert-algebra coalgebra instance,
+coalgebras on multiplicative opposites, and helper lemmas for finite sums,
+ites/dites, digit-sum divisibility in arbitrary bases, and `RCLike`-valued
+order relations.
+
+## Provenance
+
+Imported from <https://github.com/themathqueen/monlib4> (originally Lean
+`v4.21.0-rc3`) and ported to Lean Pool's `v4.30.0-rc2` / Mathlib `v4.30.0-rc2`.
+The successor of <https://github.com/themathqueen/monlib> (the Lean 3 version).
+Large parts of the upstream quantum-graph and Schur-product theorem stack are
+not yet vendored. In particular, upstream modules such as
+`QuantumGraph.OfClassicalGraph` and the deeper theorem sections of
+`QuantumSet.SchurMul` / `QuantumGraph.Basic` depend on the older
+`PiLp`/normed-ring scaffold and upstream heartbeat or linter overrides that
+Lean Pool does not permit.
+-/

LeanPool/Monlib4/LinearAlgebra.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Monica Omar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Monica Omar
+-/
+
+import LeanPool.Monlib4.LinearAlgebra.Coalgebra
+import LeanPool.Monlib4.LinearAlgebra.DirectSumFromTo
+import LeanPool.Monlib4.LinearAlgebra.End
+import LeanPool.Monlib4.LinearAlgebra.InnerAut
+import LeanPool.Monlib4.LinearAlgebra.InvariantSubmodule
+import LeanPool.Monlib4.LinearAlgebra.Ips
+import LeanPool.Monlib4.LinearAlgebra.IsProj'
+import LeanPool.Monlib4.LinearAlgebra.IsReal
+import LeanPool.Monlib4.LinearAlgebra.KroneckerToTensor
+import LeanPool.Monlib4.LinearAlgebra.LinearMapOp
+import LeanPool.Monlib4.LinearAlgebra.LmulRmul
+import LeanPool.Monlib4.LinearAlgebra.Matrix
+import LeanPool.Monlib4.LinearAlgebra.Mul''
+import LeanPool.Monlib4.LinearAlgebra.MyBimodule
+import LeanPool.Monlib4.LinearAlgebra.MySpec
+import LeanPool.Monlib4.LinearAlgebra.Nacgor
+import LeanPool.Monlib4.LinearAlgebra.OfNorm
+import LeanPool.Monlib4.LinearAlgebra.PiDirectSum
+import LeanPool.Monlib4.LinearAlgebra.PiStarOrderedRing
+import LeanPool.Monlib4.LinearAlgebra.PosMapIsReal
+import LeanPool.Monlib4.LinearAlgebra.QuantumSet
+import LeanPool.Monlib4.LinearAlgebra.TensorProduct
+import LeanPool.Monlib4.LinearAlgebra.ToMatrixOfEquiv
+
+/-!
+# LinearAlgebra
+
+Import-only index for the `LinearAlgebra` directory of the monlib4 import.
+-/

LeanPool/Monlib4/LinearAlgebra/Coalgebra.lean

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2026 Monica Omar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Monica Omar
+-/
+
+import LeanPool.Monlib4.LinearAlgebra.Coalgebra.FiniteDimensional
+import LeanPool.Monlib4.LinearAlgebra.Coalgebra.Lemmas
+import LeanPool.Monlib4.LinearAlgebra.Coalgebra.MulOpposite
+
+/-!
+# Coalgebra
+
+Import-only index for the `LinearAlgebra/Coalgebra` directory of the monlib4
+import.
+-/