Skip to content

[Merged by Bors] - chore: bump toolchain to v4.2.0-rc2#7703

Closed
kim-em wants to merge 1 commit intomasterfrom
bump-v4.2.0-rc2
Closed

[Merged by Bors] - chore: bump toolchain to v4.2.0-rc2#7703
kim-em wants to merge 1 commit intomasterfrom
bump-v4.2.0-rc2

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Oct 16, 2023

This includes all the changes from #7606.

Open in Gitpod

@kim-em kim-em added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Oct 16, 2023
@kim-em kim-em mentioned this pull request Oct 16, 2023
Closed
@PatrickMassot
Copy link
Copy Markdown
Member

PatrickMassot commented Oct 16, 2023

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Oct 16, 2023

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Oct 16, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Oct 16, 2023

!bench

@kim-em kim-em added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Oct 16, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Oct 16, 2023
@ghost
Copy link
Copy Markdown

ghost commented Oct 16, 2023

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

bors bot pushed a commit that referenced this pull request Oct 16, 2023
@kim-em
chore: bump toolchain to v4.2.0-rc2 (#7703)
26eb2b0 
This includes all the changes from #7606.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 16, 2023

Here are the benchmark results for commit d8f5691.
There were significant changes against commit 7f121a4:

  Benchmark                                                          Metric             Change
  ============================================================================================
+ build                                                              elaboration        -19.5%
+ build                                                              instructions       -11.3%
+ build                                                              interpretation      -7.9%
+ build                                                              simp                -6.9%
+ build                                                              tactic execution   -31.4%
+ build                                                              task-clock          -8.1%
+ build                                                              wall-clock         -14.4%
+ lint                                                               instructions        -7.0%
+ lint                                                               wall-clock         -10.9%
+ ~Mathlib.Algebra.Category.AlgebraCat.Limits                        instructions       -39.4%
+ ~Mathlib.Algebra.Category.AlgebraCat.Monoidal                      instructions       -29.6%
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic                        instructions       -88.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Adjunctions                    instructions       -17.1%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions        -2.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Colimits                       instructions       -45.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions       -31.5%
+ ~Mathlib.Algebra.Category.Ring.Limits                              instructions       -33.1%
+ ~Mathlib.Algebra.DirectLimit                                       instructions       -20.5%
+ ~Mathlib.Algebra.Homology.Augment                                  instructions       -16.3%
+ ~Mathlib.Algebra.Homology.DifferentialObject                       instructions        -5.5%
+ ~Mathlib.Algebra.Homology.LocalCohomology                          instructions       -77.7%
+ ~Mathlib.Algebra.Homology.ModuleCat                                instructions       -23.7%
+ ~Mathlib.Algebra.Jordan.Basic                                      instructions        -7.1%
+ ~Mathlib.Algebra.Lie.Matrix                                        instructions       -34.6%
+ ~Mathlib.Algebra.Lie.TensorProduct                                 instructions       -35.4%
+ ~Mathlib.Algebra.Lie.UniversalEnveloping                           instructions       -52.0%
+ ~Mathlib.Algebra.Lie.Weights.Cartan                                instructions       -25.3%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions        -7.4%
+ ~Mathlib.Algebra.Module.PID                                        instructions       -38.5%
+ ~Mathlib.Algebra.Module.Torsion                                    instructions       -13.2%
+ ~Mathlib.Algebra.MonoidAlgebra.Grading                             instructions       -24.7%
+ ~Mathlib.AlgebraicGeometry.AffineScheme                            instructions       -47.1%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point                     instructions       -17.6%
+ ~Mathlib.AlgebraicGeometry.FunctionField                           instructions       -26.4%
+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction                     instructions       -73.2%
+ ~Mathlib.AlgebraicGeometry.Gluing                                  instructions       -11.8%
+ ~Mathlib.AlgebraicGeometry.Morphisms.Basic                         instructions       -22.4%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated                instructions        -6.9%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties             instructions       -16.9%
+ ~Mathlib.AlgebraicGeometry.OpenImmersion                           instructions        -9.8%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf       instructions       -13.2%
+ ~Mathlib.AlgebraicGeometry.Pullbacks                               instructions       -18.6%
+ ~Mathlib.AlgebraicGeometry.Scheme                                  instructions       -50.2%
+ ~Mathlib.AlgebraicGeometry.Spec                                    instructions       -56.1%
+ ~Mathlib.AlgebraicGeometry.StructureSheaf                          instructions       -13.9%
+ ~Mathlib.Analysis.Analytic.Basic                                   instructions       -12.8%
+ ~Mathlib.Analysis.Analytic.Composition                             instructions       -17.8%
+ ~Mathlib.Analysis.Analytic.Inverse                                 instructions       -31.2%
+ ~Mathlib.Analysis.BoxIntegral.Partition.Split                      instructions       -47.5%
+ ~Mathlib.Analysis.Calculus.ContDiff                                instructions       -24.1%
+ ~Mathlib.Analysis.Calculus.ContDiffDef                             instructions       -44.7%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul                               instructions        -9.1%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic                         instructions       -41.0%
+ ~Mathlib.Analysis.Calculus.Series                                  instructions       -51.1%
+ ~Mathlib.Analysis.Complex.PhragmenLindelof                         instructions       -20.2%
+ ~Mathlib.Analysis.Complex.RealDeriv                                instructions       -19.1%
+ ~Mathlib.Analysis.Complex.UpperHalfPlane.Basic                     instructions       -53.7%
+ ~Mathlib.Analysis.Complex.UpperHalfPlane.Metric                    instructions       -12.9%
+ ~Mathlib.Analysis.Convolution                                      instructions       -17.2%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace                       instructions        -7.0%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions       -35.1%
+ ~Mathlib.Analysis.Fourier.PoissonSummation                         instructions       -50.5%
+ ~Mathlib.Analysis.Fourier.RiemannLebesgueLemma                     instructions       -48.5%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions        -9.5%
+ ~Mathlib.Analysis.InnerProductSpace.Basic                          instructions        -9.6%
+ ~Mathlib.Analysis.InnerProductSpace.Dual                           instructions       -22.9%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions        -5.5%
+ ~Mathlib.Analysis.InnerProductSpace.Projection                     instructions        -5.1%
+ ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions        -8.9%
+ ~Mathlib.Analysis.MeanInequalities                                 instructions       -43.8%
+ ~Mathlib.Analysis.NormedSpace.LpEquiv                              instructions       -23.3%
+ ~Mathlib.Analysis.NormedSpace.Multilinear                          instructions       -33.1%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions       -23.4%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions       -42.6%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions       -21.2%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions        -4.9%
+ ~Mathlib.Analysis.SpecialFunctions.Complex.Arg                     instructions       -22.8%
+ ~Mathlib.Analysis.SpecialFunctions.Gamma.Basic                     instructions       -23.2%
+ ~Mathlib.Analysis.SpecialFunctions.Gaussian                        instructions       -52.1%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv                       instructions       -13.1%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Real                        instructions       -27.8%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic             instructions       -73.4%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds            instructions       -42.6%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv             instructions       -22.4%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd     instructions       -33.7%
- ~Mathlib.CategoryTheory.Abelian.InjectiveResolution                instructions         3.4%
+ ~Mathlib.CategoryTheory.Abelian.LeftDerived                        instructions       -40.3%
+ ~Mathlib.CategoryTheory.Abelian.RightDerived                       instructions       -45.7%
- ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions         5.9%
+ ~Mathlib.CategoryTheory.Monoidal.Bimod                             instructions       -22.6%
+ ~Mathlib.CategoryTheory.Monoidal.Free.Coherence                    instructions       -25.6%
+ ~Mathlib.Combinatorics.Additive.Behrend                            instructions       -38.4%
+ ~Mathlib.Data.Matrix.Rank                                          instructions       -20.2%
+ ~Mathlib.Data.Nat.Basic                                            instructions       -53.8%
+ ~Mathlib.Data.Real.ENNReal                                         instructions        -9.9%
+ ~Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber          instructions        -5.6%
+ ~Mathlib.FieldTheory.AbelRuffini                                   instructions       -19.3%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions       -19.7%
+ ~Mathlib.FieldTheory.Cardinality                                   instructions       -70.5%
+ ~Mathlib.FieldTheory.Fixed                                         instructions       -22.1%
+ ~Mathlib.FieldTheory.Galois                                        instructions       -28.0%
+ ~Mathlib.FieldTheory.IntermediateField                             instructions       -21.3%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions       -57.3%
+ ~Mathlib.FieldTheory.IsAlgClosed.Basic                             instructions       -13.0%
+ ~Mathlib.FieldTheory.Normal                                        instructions       -12.2%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions       -23.4%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup                         instructions       -19.7%
+ ~Mathlib.FieldTheory.PrimitiveElement                              instructions       -22.0%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions       -11.0%
+ ~Mathlib.FieldTheory.SplittingField.Construction                   instructions       -51.7%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic                   instructions       -60.3%
+ ~Mathlib.Geometry.Euclidean.Angle.Sphere                           instructions       -50.7%
+ ~Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle            instructions       -46.2%
+ ~Mathlib.Geometry.Euclidean.Basic                                  instructions       -12.9%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions       -10.2%
+ ~Mathlib.Geometry.Euclidean.MongePoint                             instructions        -9.8%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions       -30.9%
+ ~Mathlib.Geometry.Manifold.ContMDiff                               instructions       -23.5%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions       -17.0%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere                        instructions       -16.8%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions        -5.2%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing               instructions        -5.8%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits          instructions       -28.9%
+ ~Mathlib.GroupTheory.FiniteAbelian                                 instructions       -53.3%
+ ~Mathlib.GroupTheory.Solvable                                      instructions       -83.4%
+ ~Mathlib.GroupTheory.SpecificGroups.Alternating                    instructions       -47.7%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineSubspace                  instructions       -17.8%
+ ~Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional               instructions       -23.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions       -49.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions       -31.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions       -28.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions       -48.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even                        instructions       -21.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions       -33.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions       -29.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions       -35.3%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions       -26.7%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions       -38.4%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions       -24.8%
+ ~Mathlib.LinearAlgebra.FiniteDimensional                           instructions        -7.2%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions        -2.9%
+ ~Mathlib.LinearAlgebra.FreeModule.Norm                             instructions       -84.2%
+ ~Mathlib.LinearAlgebra.FreeModule.StrongRankCondition              instructions       -64.9%
+ ~Mathlib.LinearAlgebra.Isomorphisms                                instructions       -25.4%
+ ~Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup                   instructions       -27.3%
+ ~Mathlib.LinearAlgebra.Orientation                                 instructions       -24.4%
+ ~Mathlib.LinearAlgebra.TensorPower                                 instructions       -35.9%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite                      instructions       -33.2%
+ ~Mathlib.LinearAlgebra.Trace                                       instructions       -11.2%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions        -9.9%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions       -10.3%
+ ~Mathlib.MeasureTheory.Function.Jacobian                           instructions       -18.4%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions       -11.8%
+ ~Mathlib.MeasureTheory.Function.UniformIntegrable                  instructions       -34.6%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions        -5.4%
+ ~Mathlib.MeasureTheory.Integral.CircleTransform                    instructions       -46.1%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral                        instructions       -13.6%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions        -7.5%
+ ~Mathlib.MeasureTheory.MeasurableSpace.Card                        instructions       -73.7%
+ ~Mathlib.MeasureTheory.Measure.Hausdorff                           instructions       -15.2%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions        -6.7%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions       -22.6%
+ ~Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure            instructions       -73.3%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions       -12.7%
+ ~Mathlib.NumberTheory.Cyclotomic.Rat                               instructions       -12.0%
+ ~Mathlib.NumberTheory.KummerDedekind                               instructions       -28.6%
+ ~Mathlib.NumberTheory.LegendreSymbol.GaussSum                      instructions       -43.5%
+ ~Mathlib.NumberTheory.LegendreSymbol.ZModChar                      instructions       -90.6%
+ ~Mathlib.NumberTheory.LucasLehmer                                  instructions       -38.7%
+ ~Mathlib.NumberTheory.Modular                                      instructions       -32.2%
+ ~Mathlib.NumberTheory.ModularForms.Basic                           instructions       -72.7%
+ ~Mathlib.NumberTheory.ModularForms.CongruenceSubgroups             instructions       -68.9%
+ ~Mathlib.NumberTheory.ModularForms.SlashActions                    instructions       -65.1%
+ ~Mathlib.NumberTheory.NumberField.Basic                            instructions       -16.7%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions        -9.2%
+ ~Mathlib.NumberTheory.NumberField.Norm                             instructions       -19.0%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions       -14.7%
+ ~Mathlib.NumberTheory.Padics.PadicIntegers                         instructions       -22.8%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions        -4.1%
+ ~Mathlib.NumberTheory.SumFourSquares                               instructions       -38.8%
+ ~Mathlib.NumberTheory.ZetaFunction                                 instructions       -29.5%
+ ~Mathlib.NumberTheory.ZetaValues                                   instructions       -25.9%
+ ~Mathlib.Probability.Variance                                      instructions       -21.8%
+ ~Mathlib.RepresentationTheory.Character                            instructions       -15.9%
+ ~Mathlib.RepresentationTheory.FdRep                                instructions       -54.9%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Basic                instructions       -90.5%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution           instructions       -34.4%
+ ~Mathlib.RepresentationTheory.Rep                                  instructions       -33.2%
+ ~Mathlib.RingTheory.Adjoin.Field                                   instructions       -47.4%
+ ~Mathlib.RingTheory.AdjoinRoot                                     instructions       -12.1%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions       -12.6%
+ ~Mathlib.RingTheory.ClassGroup                                     instructions        -9.3%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions       -18.8%
+ ~Mathlib.RingTheory.DedekindDomain.IntegralClosure                 instructions       -19.8%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions       -20.2%
+ ~Mathlib.RingTheory.Finiteness                                     instructions       -49.7%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions       -13.0%
+ ~Mathlib.RingTheory.Ideal.Norm                                     instructions       -33.0%
+ ~Mathlib.RingTheory.IntegralClosure                                instructions       -15.2%
+ ~Mathlib.RingTheory.Jacobson                                       instructions       -61.1%
+ ~Mathlib.RingTheory.JacobsonIdeal                                  instructions       -40.7%
+ ~Mathlib.RingTheory.Kaehler                                        instructions       -36.7%
+ ~Mathlib.RingTheory.LocalProperties                                instructions       -42.9%
+ ~Mathlib.RingTheory.MatrixAlgebra                                  instructions       -40.7%
+ ~Mathlib.RingTheory.Norm                                           instructions        -9.2%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions       -29.7%
+ ~Mathlib.RingTheory.Polynomial.Hermite.Basic                       instructions       -37.2%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions       -16.7%
+ ~Mathlib.RingTheory.TensorProduct                                  instructions        -9.5%
+ ~Mathlib.RingTheory.Trace                                          instructions       -10.5%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions       -10.1%
+ ~Mathlib.RingTheory.WittVector.InitTail                            instructions       -85.8%
+ ~Mathlib.RingTheory.WittVector.IsPoly                              instructions       -52.8%
+ ~Mathlib.SetTheory.Game.Birthday                                   instructions       -31.6%
+ ~Mathlib.SetTheory.Ordinal.NaturalOps                              instructions       -47.0%
+ ~Mathlib.SetTheory.ZFC.Basic                                       instructions       -42.8%
+ ~Mathlib.Topology.ContinuousFunction.Ideals                        instructions       -22.2%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions       -15.6%
+ ~Mathlib.Topology.EMetricSpace.Basic                               instructions       -18.4%
+ ~Mathlib.Topology.Instances.ENNReal                                instructions       -14.0%
+ ~Mathlib.Topology.MetricSpace.GromovHausdorff                      instructions        -7.3%
+ ~Mathlib.Topology.Sheaves.Stalks                                   instructions       -11.3%
+ ~Mathlib.Topology.TietzeExtension                                  instructions       -34.7%

@bors
Copy link
Copy Markdown

bors bot commented Oct 16, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: bump toolchain to v4.2.0-rc2 [Merged by Bors] - chore: bump toolchain to v4.2.0-rc2 Oct 16, 2023
@bors bors bot closed this Oct 16, 2023
@bors bors bot deleted the bump-v4.2.0-rc2 branch October 16, 2023 04:42
mattrobball added a commit that referenced this pull request Oct 16, 2023
@mattrobball
Revert "chore: bump toolchain to v4.2.0-rc2 (#7703)"
87e1348 
This reverts commit 26eb2b0.
bors bot pushed a commit that referenced this pull request Oct 16, 2023
@mattrobball
chore: revert #7703 (#7710)
f3695eb 
This reverts commit 26eb2b0.
@kim-em kim-em mentioned this pull request Oct 16, 2023
Merged
kim-em added a commit that referenced this pull request Oct 17, 2023
@kim-em
Revert "chore: revert #7703 (#7710)"
ab56fa2 
This reverts commit f3695eb.
@urkud urkud mentioned this pull request May 5, 2024
Closed
eric-wieser
eric-wieser reviewed Sep 15, 2025
View reviewed changes
Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
* `ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense`: The adjoint on
`ContinuousLinearMap` and `LinearPMap` coincide.
* `LinearPMap.adjoint_isClosed`: The adjoint is a closed operator.
* `IsSelfAdjoint.isClosed`: Every self-adjoint operator is closed.
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Sep 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just flagging what seems to be an accidental deletion

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

Assignees

No one assigned

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@kim-em @PatrickMassot @leanprover-bot @eric-wieser