[Merged by Bors] - feature(Analysis/LocallyConvex/Polar): Show that the polar is weak*-closed and absolutely convex by mans0954 · Pull Request #21002 · leanprover-community/mathlib4

mans0954 · 2025-01-23T21:28:50Z

Show that the absolute polar is weak*-closed and absolutely convex.

Via closedAbsConvexHull_min this establishes the easy direction of the Bipolar Theorem #20843

depends on: [Merged by Bors] - feature(Analysis/Seminorm): Add closedBall equivalents of open ball results #22264
depends on: [Merged by Bors] - feature(Analysis/LocallyConvex/Polar): Polar is weak*-closed #22352

github-actions · 2025-01-23T21:29:42Z

PR summary dc1aa396bb

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Module.Dual	1842	1846	+4 (+0.22%)

Import changes for all files

Files	Import difference
165 files `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.CStarAlgebra.PositiveLinearMap` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Complex.Liouville` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.Positivity` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.Analysis.Convex.Integral` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.Analysis.Fourier.AddCircleMulti` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Analysis.SpecialFunctions.Gamma.Deriv` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.Analysis.SpecialFunctions.Integrals` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.Analysis.SpecialFunctions.Log.Summable` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine` `Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle` `Mathlib.Geometry.Euclidean.Angle.Sphere` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.Geometry.Manifold.Complex` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.InformationTheory.KullbackLeibler.Basic` `Mathlib.InformationTheory.KullbackLeibler.KLFun` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.NumberTheory.AbelSummation` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.Positivity` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.NumberTheory.LSeries.SumCoeff` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.Probability.Distributions.Pareto` `Mathlib.Probability.Moments.ComplexMGF` `Mathlib.Probability.Moments.MGFAnalytic` `Mathlib.Probability.Moments.SubGaussian` `Mathlib.Probability.Moments.Tilted` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic`	2
76 files `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Analysis.Convex.Cone.Proper` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Dynamics.Ergodic.RadonNikodym` `Mathlib.Geometry.Euclidean.Angle.Oriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Real` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.MeasureTheory.Function.FactorsThrough` `Mathlib.MeasureTheory.Integral.FundThmCalculus` `Mathlib.MeasureTheory.Integral.IntegrationByParts` `Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.CDF` `Mathlib.Probability.CondVar` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Probability.Density` `Mathlib.Probability.Distributions.Uniform` `Mathlib.Probability.IdentDistrib` `Mathlib.Probability.Independence.Conditional` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Probability.Kernel.CompProdEqIff` `Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.Probability.Kernel.IonescuTulcea.Traj` `Mathlib.Probability.Kernel.Posterior` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.Probability.Martingale.Basic` `Mathlib.Probability.Martingale.BorelCantelli` `Mathlib.Probability.Martingale.Centering` `Mathlib.Probability.Martingale.Convergence` `Mathlib.Probability.Martingale.OptionalSampling` `Mathlib.Probability.Martingale.OptionalStopping` `Mathlib.Probability.Martingale.Upcrossing` `Mathlib.Probability.Moments.Basic` `Mathlib.Probability.Notation` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Process.Filtration` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Process.Stopping` `Mathlib.Probability.ProductMeasure` `Mathlib.Probability.StrongLaw` `Mathlib.Probability.Variance`	3
6 files `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.Analysis.InnerProductSpace.LaxMilgram` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.Analysis.Normed.Module.Dual` `Mathlib.Analysis.Normed.Module.WeakDual`	4

Declarations diff

+ AbsConvex.iInter₂
+ Balanced.mulActionHom_preimage
+ polar_AbsConvex

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mans0954 · 2025-01-29T19:52:27Z

Oops - forgot to remove the WIP label.

Mathlib/Analysis/Convex/Basic.lean

Mathlib/Analysis/LocallyConvex/Basic.lean

Mathlib/Analysis/LocallyConvex/Polar.lean

Co-authored-by: Jireh Loreaux <[email protected]>

j-loreaux · 2025-02-15T04:23:26Z

The import increase is unacceptably large. Can you try to find a better place with #find_home? Probably something in Analysis.Normed is the way to go, but I'm not certain.

mans0954 · 2025-03-01T07:22:11Z

@j-loreaux the large-import label has been removed from the PR now, so please are you able to take another look?

Mathlib/Analysis/LocallyConvex/Basic.lean

Mathlib/Analysis/Normed/Module/Dual.lean

Co-authored-by: Jireh Loreaux <[email protected]>

This reverts commit f8148c2.

Co-authored-by: Jireh Loreaux <[email protected]>

j-loreaux

I think the import increase is okay, as this result does belong in this file, but we'll see what someone else says:

maintainer merge

github-actions · 2025-04-07T16:42:25Z

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

jcommelin

Thanks 🎉

bors merge

…losed and absolutely convex (#21002) Show that the absolute polar is weak*-closed and absolutely convex. Via `closedAbsConvexHull_min` this establishes the easy direction of the Bipolar Theorem #20843 Co-authored-by: Christopher Hoskin <[email protected]>

mathlib-bors · 2025-04-08T04:43:05Z

Pull request successfully merged into master.

Build succeeded:

mans0954 · 2025-04-09T07:42:48Z

I think the import increase is okay, as this result does belong in this file, but we'll see what someone else says:

I've ended up creating a new file for the bipolar theorem as that has extra imports. Possibly we could move polar_AbsConvex in there: eb6e4bd ?

…losed and absolutely convex (#21002) Show that the absolute polar is weak*-closed and absolutely convex. Via `closedAbsConvexHull_min` this establishes the easy direction of the Bipolar Theorem #20843 Co-authored-by: Christopher Hoskin <[email protected]>

…which is no longer needed

Show that the polar is absolutely convex

d748d4b

mans0954 added the WIP Work in progress label Jan 23, 2025

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 23, 2025

github-actions bot added the t-analysis Analysis (normed *, calculus) label Jan 23, 2025

mans0954 changed the title ~~Show that the polar is absolutely convex~~ feature(Analysis/LocallyConvex/Polar): Show that the polar is absolutely convex Jan 23, 2025

polar weak*-closed

6f3e978

mans0954 mentioned this pull request Jan 23, 2025

feature(Analysis/LocallyConvex/Polar): Bipolar theorem #20843

Closed

2 tasks

mans0954 changed the title ~~feature(Analysis/LocallyConvex/Polar): Show that the polar is absolutely convex~~ feature(Analysis/LocallyConvex/Polar): Show that the polar is weak*-closed and absolutely convex Jan 23, 2025

Add example

f6d0515

mans0954 marked this pull request as ready for review January 23, 2025 22:28

mans0954 removed the WIP Work in progress label Jan 29, 2025

mans0954 added 2 commits January 31, 2025 20:59

Merge branch 'master' into mans0954/polar_AbsConvex

89d7fca

Merge branch 'master' into mans0954/polar_AbsConvex

3a62f7b

j-loreaux reviewed Feb 14, 2025

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 14, 2025

mans0954 and others added 9 commits February 14, 2025 19:10

Update Mathlib/Analysis/LocallyConvex/Basic.lean

bd78beb

Co-authored-by: Jireh Loreaux <[email protected]>

Update Mathlib/Analysis/LocallyConvex/Polar.lean

a22f6f0

Co-authored-by: Jireh Loreaux <[email protected]>

Update Mathlib/Analysis/LocallyConvex/Polar.lean

1680b04

Co-authored-by: Jireh Loreaux <[email protected]>

Fix

5a1d537

Bipolar theorem

4bae0da

Make Convex.is_linear_preimage more general

43c2122

Fix

b8889bf

Merge branch 'master' into mans0954/polar_AbsConvex

2a95f50

Fix

8938589

mans0954 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 14, 2025

mans0954 requested a review from j-loreaux February 14, 2025 21:48

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 15, 2025

github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Mar 1, 2025

j-loreaux reviewed Mar 1, 2025

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 1, 2025

mans0954 and others added 9 commits March 2, 2025 09:18

Update Mathlib/Analysis/LocallyConvex/Basic.lean

f8148c2

Co-authored-by: Jireh Loreaux <[email protected]>

Revert "Update Mathlib/Analysis/LocallyConvex/Basic.lean"

ef62918

This reverts commit f8148c2.

Update Mathlib/Analysis/Normed/Module/Dual.lean

93f8401

Co-authored-by: Jireh Loreaux <[email protected]>

Save the bipolar theorem to later

c7069a7

Merge branch 'master' into mans0954/polar_AbsConvex

8e4925c

Merge branch 'master' into mans0954/polar_AbsConvex

c968034

Update Mathlib/Analysis/LocallyConvex/Basic.lean

cd6d3fa

Co-authored-by: Jireh Loreaux <[email protected]>

Get it building again

af0c3ff

Better

dc1aa39

mans0954 requested a review from j-loreaux April 5, 2025 09:34

mans0954 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 5, 2025

j-loreaux approved these changes Apr 7, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 7, 2025

jcommelin reviewed Apr 8, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 8, 2025

mathlib-bors bot changed the title ~~feature(Analysis/LocallyConvex/Polar): Show that the polar is weak*-closed and absolutely convex~~ [Merged by Bors] - feature(Analysis/LocallyConvex/Polar): Show that the polar is weak*-closed and absolutely convex Apr 8, 2025

mathlib-bors bot closed this Apr 8, 2025

mathlib-bors bot deleted the mans0954/polar_AbsConvex branch April 8, 2025 04:43

mans0954 added a commit to mans0954/mathlib4 that referenced this pull request Sep 6, 2025

Revert the additional complexity added in leanprover-community#21002 …

364684d

…which is no longer needed

Conversation

mans0954 commented Jan 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary dc1aa396bb

Import changes for modified files

Declarations diff

Uh oh!

mans0954 commented Jan 29, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

j-loreaux commented Feb 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mans0954 commented Mar 1, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Apr 7, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Apr 8, 2025

Uh oh!

mans0954 commented Apr 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

mans0954 commented Jan 23, 2025 •

edited

Loading

github-actions bot commented Jan 23, 2025 •

edited

Loading

j-loreaux commented Feb 15, 2025 •

edited

Loading