feat(LinearAlgebra/Matrix/ConjTranspose): conjTranspose as an AlgEquiv#37222
Open
SnirBroshi wants to merge 1 commit intoleanprover-community:masterfrom
Open
feat(LinearAlgebra/Matrix/ConjTranspose): conjTranspose as an AlgEquiv#37222SnirBroshi wants to merge 1 commit intoleanprover-community:masterfrom
conjTranspose as an AlgEquiv#37222SnirBroshi wants to merge 1 commit intoleanprover-community:masterfrom
Conversation
PR summary 93349c600f
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.LinearAlgebra.Matrix.ConjTranspose | 978 | 981 | +3 (+0.31%) |
Import changes for all files
| Files | Import difference |
|---|---|
8 filesMathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.Combinatorics.Configuration Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.LinearAlgebra.Matrix.Rank Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.LinearAlgebra.SesquilinearForm.Star |
1 |
264 filesMathlib.Algebra.AffineMonoid.Embedding Mathlib.Algebra.AffineMonoid.UniqueSums Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.FGModuleCat.Abelian Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Colimits Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Jordan.Basic Mathlib.Algebra.Lie.Abelian Mathlib.Algebra.Lie.AdjointAction.Derivation Mathlib.Algebra.Lie.BaseChange Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Classical Mathlib.Algebra.Lie.Cochain Mathlib.Algebra.Lie.Derivation.BaseChange Mathlib.Algebra.Lie.Derivation.Basic Mathlib.Algebra.Lie.DirectSum Mathlib.Algebra.Lie.Extension Mathlib.Algebra.Lie.Free Mathlib.Algebra.Lie.Graded Mathlib.Algebra.Lie.IdealOperations Mathlib.Algebra.Lie.Ideal Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Loop Mathlib.Algebra.Lie.Matrix Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Normalizer Mathlib.Algebra.Lie.OfAssociative Mathlib.Algebra.Lie.Prod Mathlib.Algebra.Lie.Quotient Mathlib.Algebra.Lie.SemiDirect Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.SerreConstruction Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Algebra.Lie.Sl2 Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.Subalgebra Mathlib.Algebra.Lie.Submodule Mathlib.Algebra.Lie.TensorProduct Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.Algebra.LieRinehartAlgebra.Defs Mathlib.Algebra.Module.Lattice Mathlib.Algebra.Module.SpanRankOperations Mathlib.Algebra.Module.Submodule.Union Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.MvPolynomial.Nilpotent Mathlib.Algebra.QuadraticAlgebra.NormDeterminant Mathlib.Algebra.Star.LinearMap Mathlib.Algebra.Symmetrized Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Convex.BetweenList Mathlib.Analysis.Convex.Between Mathlib.Analysis.Convex.Radon Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.Visible Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.Normed.Module.Bases Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.ContinuousInverse Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.Data.ZMod.QuotientRing Mathlib.Dynamics.Newton Mathlib.Geometry.Convex.Cone.TensorProduct Mathlib.Geometry.Polygon.Basic Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Coevaluation Mathlib.LinearAlgebra.Complex.Determinant Mathlib.LinearAlgebra.Complex.FiniteDimensional Mathlib.LinearAlgebra.Complex.Module Mathlib.LinearAlgebra.Complex.Orientation Mathlib.LinearAlgebra.Contraction Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Dual.BaseChange Mathlib.LinearAlgebra.Dual.Lemmas Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.LinearAlgebra.ExteriorAlgebra.Basis Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.LinearAlgebra.ExteriorPower.Basis Mathlib.LinearAlgebra.ExteriorPower.Pairing Mathlib.LinearAlgebra.FiniteDimensional.Basic Mathlib.LinearAlgebra.FiniteDimensional.Lemmas Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient Mathlib.LinearAlgebra.FreeModule.Finite.Quotient Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.LinearAlgebra.FreeModule.Int Mathlib.LinearAlgebra.FreeModule.PID Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv Mathlib.LinearAlgebra.Lagrange Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.LinearAlgebra.Matrix.Basis Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.LinearAlgebra.Matrix.Kronecker Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.LinearAlgebra.Matrix.Vec Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.PerfectPairing.Basic Mathlib.LinearAlgebra.PerfectPairing.Restrict Mathlib.LinearAlgebra.Projectivization.Action Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.LinearAlgebra.QuadraticForm.Radical Mathlib.LinearAlgebra.QuadraticForm.Signature Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.LinearAlgebra.Span.TensorProduct Mathlib.LinearAlgebra.SymplecticGroup Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.LinearAlgebra.UnitaryGroup Mathlib.LinearAlgebra.Vandermonde Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.ModelTheory.Arithmetic.Presburger.Definability Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic Mathlib.NumberTheory.FrobeniusNumber Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.Probability.Independence.Process.HasIndepIncrements Mathlib.RepresentationTheory.Action Mathlib.RepresentationTheory.Basic Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.Equiv Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Intertwining Mathlib.RepresentationTheory.Maschke Mathlib.RepresentationTheory.Rep.Basic Mathlib.RepresentationTheory.Rep.Iso Mathlib.RepresentationTheory.Rep.Res Mathlib.RepresentationTheory.Semisimple Mathlib.RepresentationTheory.Submodule Mathlib.RepresentationTheory.Subrepresentation Mathlib.RingTheory.AdicCompletion.Completeness Mathlib.RingTheory.Artinian.Algebra Mathlib.RingTheory.Artinian.Instances Mathlib.RingTheory.Artinian.Module Mathlib.RingTheory.Artinian.Ring Mathlib.RingTheory.Derivation.Lie Mathlib.RingTheory.Extension.Cotangent.Free Mathlib.RingTheory.Extension.Presentation.Core Mathlib.RingTheory.Extension.Presentation.Submersive Mathlib.RingTheory.FiniteLength Mathlib.RingTheory.Finiteness.NilpotentKer Mathlib.RingTheory.Finiteness.Nilpotent Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Ideal.AssociatedPrime.Localization Mathlib.RingTheory.Ideal.NatInt Mathlib.RingTheory.Ideal.Pure Mathlib.RingTheory.Ideal.Quotient.Nilpotent Mathlib.RingTheory.KrullDimension.Basic Mathlib.RingTheory.KrullDimension.Field Mathlib.RingTheory.KrullDimension.NonZeroDivisors Mathlib.RingTheory.Length Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.Quotient Mathlib.RingTheory.MvPolynomial.Expand Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic Mathlib.RingTheory.MvPowerSeries.Expand Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Polynomial.DegreeLT Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.RingTheory.PowerSeries.Expand Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.Regular.Flat Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.SimpleModule.Rank Mathlib.RingTheory.SimpleModule.WedderburnArtin Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Spectrum.Maximal.Localization Mathlib.RingTheory.Spectrum.Prime.Basic Mathlib.RingTheory.Spectrum.Prime.RingHom Mathlib.RingTheory.Support Mathlib.RingTheory.TensorProduct.Free Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight Mathlib.RingTheory.TensorProduct.IsBaseChangeHom Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.RingTheory.ZMod Mathlib.Topology.Algebra.AsymptoticCone Mathlib.Topology.Algebra.Module.Determinant Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Module.TopDualPairing Mathlib.Topology.Algebra.Star.LinearMap Mathlib.Topology.Instances.Matrix |
2 |
28 filesMathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.Cartan Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Reflection Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length Mathlib.GroupTheory.Coxeter.Matrix Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.ConjTranspose Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.Hadamard Mathlib.LinearAlgebra.Matrix.Notation Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Matrix.RowCol Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Matrix.Transvection |
3 |
Declarations diff
+ conjTransposeAlgEquiv
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib-dependent-issues
bot
added
blocked-by-other-PR
|
This PR/issue depends on: |
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
SnirBroshi
force-pushed
the
feature/matrix/conj-transpose-alg-equiv
branch
from
222cdcc to
cdd8773
Compare
github-actions
bot
removed
the
merge-conflict
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wrap
Matrix.conjTransposeas aStarAlgEquivto the opposite ring.Also upgrade the existing
RingEquivto aStarRingEquiv.This relies on
TrivialStar R(the matrix has entries inαwhich is anR-algebra) because anAlgEquivrequiresf (r • M) = r • (f M)butconjTransposegives(r • M)ᴴ = (star r) • Mᴴ.Unlike
LinearEquivthere doesn't seem to be a "semilinear" variant of it overstarRingEnd.where#37178