[Merged by Bors] - feat: notation for vectors in Euclidean space by eric-wieser · Pull Request #17732 · leanprover-community/mathlib4

eric-wieser · 2024-10-14T14:01:33Z

This adds !₂[1, 2, 3] notation for (WithLp.equiv 2 (∀ _ : Fin 3, _)).symm ![1, 2, 3], which is a term of type EuclideanSpace 𝕜 (Fin 3); and more generally for other Lp norms, using the subscript parser.

This reduces the temptation to write the type-incorrect ![1, 2, 3] that has the wrong norm.

The (parser for the) subscript parser relies on initializers running, and so a missing Lean.enableInitializersExecution has to be inserted in checkYaml.lean. It has already been inserted in the necessary places in upstream repos.

Notation Zulip poll.

github-actions · 2024-10-14T14:02:19Z

PR summary 83e83066c0

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.InnerProductSpace.PiL2	1803	1804	+1 (+0.06%)
Mathlib.Analysis.Quaternion	1805	1806	+1 (+0.06%)

Import changes for all files

Files	Import difference
270 files `Mathlib.Analysis.BoxIntegral.UnitPartition` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.Analysis.SpecialFunctions.Integrals` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.Analysis.Calculus.BumpFunction.Convolution` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.NumberTheory.GaussSum` `Mathlib.MeasureTheory.Measure.Lebesgue.Complex` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.MeasureTheory.Integral.IntervalIntegral` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.InnerProductSpace.ProdL2` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.Geometry.Manifold.Complex` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.Probability.StrongLaw` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Measure.LevyProkhorovMetric` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.Probability.Kernel.Composition` `Mathlib.Analysis.RCLike.Inner` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.MeasureTheory.Integral.FundThmCalculus` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.MeasureTheory.Measure.Portmanteau` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.MeasureTheory.Measure.Haar.NormedSpace` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.NumberTheory.NumberField.Completion` `Mathlib.Probability.Kernel.WithDensity` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Geometry.Euclidean.Angle.Oriented.Basic` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.MeasureTheory.Measure.Hausdorff` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.MeasureTheory.Measure.Haar.Unique` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.Geometry.Euclidean.Angle.Sphere` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Probability.Kernel.IntegralCompProd` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace` `Mathlib.MeasureTheory.Integral.Prod` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.MeasureTheory.Covering.OneDim` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.NumberTheory.FLT.Three` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.Probability.Kernel.Invariance` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Probability.Distributions.Uniform` `Mathlib.MeasureTheory.Constructions.UnitInterval` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.Topology.CWComplex` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.Combinatorics.Additive.Randomisation` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.Fermat` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.Analysis.Quaternion` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.Probability.Kernel.Disintegration.Basic` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Analysis.Complex.Liouville` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.NumberTheory.LSeries.Positivity` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.Analysis.Convex.Measure` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.Topology.MetricSpace.HausdorffDimension` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.InnerProductSpace.PiL2` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality` `Mathlib.Analysis.ConstantSpeed` `Mathlib.LinearAlgebra.Matrix.Hermitian` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.Probability.Kernel.MeasureCompProd` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Analysis.Complex.Positivity` `Mathlib.Analysis.Fourier.FourierTransform` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.Analysis.Matrix` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.Convolution` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Analysis.BoundedVariation` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.NumberTheory.WellApproximable` `Mathlib.MeasureTheory.Measure.Lebesgue.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.Convex.Cone.Proper` `Mathlib.Probability.Distributions.Pareto` `Mathlib.MeasureTheory.Measure.Lebesgue.Integral` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Calculus.BumpFunction.InnerProduct` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.NumberTheory.NumberField.House` `Mathlib.Analysis.InnerProductSpace.l2Space` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.MeasureTheory.Integral.Periodic` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Probability.Kernel.Condexp` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Probability.Density` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.Analysis.InnerProductSpace.Orientation` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.Tactic` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.Analysis.SpecialFunctions.Gamma.Deriv` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.Probability.Independence.Conditional` `Mathlib.NumberTheory.AbelSummation` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.Probability.CDF` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.MeasureTheory.Measure.Haar.OfBasis` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.MeasureTheory.Measure.Haar.Quotient` `Mathlib.Geometry.Manifold.Instances.Sphere`	1

Declarations diff

+ EuclideanSpace.delabVecNotation

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).

eric-wieser · 2024-10-16T22:48:38Z

@digama0, any idea what's up with uncaught exception: parser 'subscript' was not found in the CI logs for lake exe check-yaml?

digama0 · 2024-10-16T23:08:56Z

My guess is that one of the linters is elaborating something in an empty environment, and it's failing to interpret the syntax objects. See 6ed0fa63 which was about a similar issue.

eric-wieser · 2024-10-17T00:25:09Z

Here there's no panic to speak of, and the issue seems to be just a regular IO exception being thrown.

I don't think linters are to blame, since adding

Lean.Elab.Command.lintersRef.set #[]

to the start of main doesn't help.

…an_notation

eric-wieser · 2024-11-14T00:26:21Z

@digama0, I think these lines are somehow not running:

mathlib4/Mathlib/Util/Superscript.lean

Lines 279 to 285 in 85ec5bf

    
           initialize 
        
             registerAlias `superscript ``superscript superscript 
        
             registerAliasCore Formatter.formatterAliasesRef `superscript superscript.formatter 
        
             registerAliasCore Parenthesizer.parenthesizerAliasesRef `superscript superscript.parenthesizer 
        
             registerAlias `subscript ``subscript subscript 
        
             registerAliasCore Formatter.formatterAliasesRef `subscript subscript.formatter 
        
             registerAliasCore Parenthesizer.parenthesizerAliasesRef `subscript subscript.parenthesizer

This is needed by leanprover-community/mathlib4#17732

…an_notation

Vierkantor · 2024-11-29T15:30:22Z

MathlibTest/EuclideanSpace.lean

+end var
+
+section tombstoned_var
+-- the point of this test is to


This comment appears unfinished.

... check if the reviewers are paying attention :). I've completed this comment.

Vierkantor

Please update the PR description to reflect all the fancy new features for this notation :)

Vierkantor

Thanks!

bors d+

Mathlib/Analysis/InnerProductSpace/PiL2.lean

mathlib-bors · 2024-12-02T14:44:04Z

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

This adds `!₂[1, 2, 3]` notation for `(WithLp.equiv 2 (∀ _ : Fin 3, _)).symm ![1, 2, 3]`, which is a term of type `EuclideanSpace 𝕜 (Fin 3)`; and more generally for other Lp norms, using the `subscript` parser. This reduces the temptation to write the type-incorrect `![1, 2, 3]` that has the wrong norm. The (parser for the) `subscript` parser relies on `initialize`rs running, and so a missing `Lean.enableInitializersExecution` has to be inserted in `checkYaml.lean`. It has already been inserted in the necessary places in upstream repos. [Notation Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Notation.20for.20vectors.20in.20euclidean.20space/near/476796192). Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2024-12-02T17:40:34Z

Pull request successfully merged into master.

Build succeeded:

We provide macros for the following notations: - `⦋m⦌ₙ` denotes the `m`-dimensional simplex in the `n`-truncated simplex category. - `X _⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated simplicial object `X`. - `X ^⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated cosimplicial object `X`. For all of these notations, the truncation proof `p : m ≤ n` can also be provided using the syntax `⦋m, p⦌ₙ`, `X _⦋m, p⦌ₙ`, and `X ^⦋m, p⦌ₙ`, respectively. These notations generalize those already in use in `HomotopyCat.lean` and `Coskeletal.lean`. Delaborators for these notations are added in #20719. See #17732 and #20355 to understand the reason for the use of `subscriptTerm`. Co-authored-by: gio256 <gio256@protonmail.com>

…ommunity#20688) We provide macros for the following notations: - `⦋m⦌ₙ` denotes the `m`-dimensional simplex in the `n`-truncated simplex category. - `X _⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated simplicial object `X`. - `X ^⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated cosimplicial object `X`. For all of these notations, the truncation proof `p : m ≤ n` can also be provided using the syntax `⦋m, p⦌ₙ`, `X _⦋m, p⦌ₙ`, and `X ^⦋m, p⦌ₙ`, respectively. These notations generalize those already in use in `HomotopyCat.lean` and `Coskeletal.lean`. Delaborators for these notations are added in leanprover-community#20719. See leanprover-community#17732 and leanprover-community#20355 to understand the reason for the use of `subscriptTerm`. Co-authored-by: gio256 <gio256@protonmail.com>

feat: notation for Euclidean space

94b264d

github-actions bot added the t-analysis Analysis (normed *, calculus) label Oct 14, 2024

eric-wieser mentioned this pull request Oct 14, 2024

Add missing informal + Lean statements for four missing problems trishullab/PutnamBench#226

Merged

eric-wieser added the awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there label Oct 14, 2024

numeral

daf8ace

eric-wieser removed the awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there label Oct 26, 2024

Merge remote-tracking branch 'origin/master' into eric-wieser/euclide…

a577e9a

…an_notation

fix yaml processing

e84a8f3

eric-wieser added a commit to leanprover-community/import-graph that referenced this pull request Nov 14, 2024

fix: run Lean.enableInitializersExecution before importing modules

c9ac6d4

This is needed by leanprover-community/mathlib4#17732

eric-wieser mentioned this pull request Nov 14, 2024

fix: run Lean.enableInitializersExecution before importing modules leanprover-community/import-graph#44

Merged

eric-wieser added 3 commits November 18, 2024 19:20

Merge remote-tracking branch 'origin/master' into eric-wieser/euclide…

070885a

…an_notation

Merge remote-tracking branch 'origin/master' into eric-wieser/euclide…

d735481

…an_notation

shake

93ee631

eric-wieser requested a review from Vierkantor November 22, 2024 21:32

Vierkantor reviewed Nov 29, 2024

View reviewed changes

Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 29, 2024

Update EuclideanSpace.lean

e92b7e3

eric-wieser removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 29, 2024

eric-wieser requested a review from Vierkantor November 29, 2024 22:34

eric-wieser changed the title ~~feat: notation for Euclidean space~~ feat: notation for vectors in Euclidean space Nov 29, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 1, 2024

Merge branch 'master' into eric-wieser/euclidean_notation

aace520

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 1, 2024

Vierkantor approved these changes Dec 2, 2024

View reviewed changes

Mathlib/Analysis/InnerProductSpace/PiL2.lean Outdated Show resolved Hide resolved

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Dec 2, 2024

eric-wieser added 2 commits December 2, 2024 17:11

Update PiL2.lean

b13ef96

Update PiL2.lean

83e8306

ghost added the ready-to-merge This PR has been sent to bors. label Dec 2, 2024

mathlib-bors bot changed the title ~~feat: notation for vectors in Euclidean space~~ [Merged by Bors] - feat: notation for vectors in Euclidean space Dec 2, 2024

mathlib-bors bot closed this Dec 2, 2024

mathlib-bors bot deleted the eric-wieser/euclidean_notation branch December 2, 2024 17:40

gio256 mentioned this pull request Jan 12, 2025

[Merged by Bors] - feat(AlgebraicTopology): truncated simplicial notations #20688

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: notation for vectors in Euclidean space#17732

[Merged by Bors] - feat: notation for vectors in Euclidean space#17732
eric-wieser wants to merge 11 commits intomasterfrom
eric-wieser/euclidean_notation

eric-wieser commented Oct 14, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Oct 14, 2024 •

edited

Loading

Import changes for modified files

Uh oh!

eric-wieser commented Oct 16, 2024

Uh oh!

digama0 commented Oct 16, 2024

Uh oh!

eric-wieser commented Oct 17, 2024

Uh oh!

eric-wieser commented Nov 14, 2024

Uh oh!

Vierkantor Nov 29, 2024

Uh oh!

eric-wieser Nov 29, 2024

Uh oh!

Vierkantor left a comment

Uh oh!

Vierkantor left a comment

Uh oh!

Uh oh!

mathlib-bors bot commented Dec 2, 2024

Uh oh!

mathlib-bors bot commented Dec 2, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

eric-wieser commented Oct 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 83e83066c0

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser commented Oct 16, 2024

Uh oh!

digama0 commented Oct 16, 2024

Uh oh!

eric-wieser commented Oct 17, 2024

Uh oh!

eric-wieser commented Nov 14, 2024

Uh oh!

Vierkantor Nov 29, 2024

Choose a reason for hiding this comment

Uh oh!

eric-wieser Nov 29, 2024

Choose a reason for hiding this comment

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Dec 2, 2024

Uh oh!

mathlib-bors bot commented Dec 2, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

eric-wieser commented Oct 14, 2024 •

edited

Loading

github-actions bot commented Oct 14, 2024 •

edited

Loading