Skip to content

[Merged by Bors] - chore: update deprecated declarations in *.yamls #38312

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
thorimur wants to merge 1 commit into from
+11 −12
Closed

[Merged by Bors] - chore: update deprecated declarations in *.yamls #38312

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions docs/1000.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3506,7 +3506,7 @@ Q6799039:

Q6813106:
title: Mellin inversion theorem
decl: mellin_inversion
decl: mellinInv_mellin_eq

Q6859627:
title: Milliken's tree theorem
Expand Down Expand Up @@ -3623,7 +3623,6 @@ Q7208500:
title: Poisson limit theorem
decls:
- ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop
- ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTop
authors: Yi Yuan
date: 2026

Expand Down
12 changes: 6 additions & 6 deletions docs/overview.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ General algebra:
presheafed space: 'AlgebraicGeometry.PresheafedSpace'
sheafed space: 'AlgebraicGeometry.SheafedSpace'
monoidal category: 'CategoryTheory.MonoidalCategory'
Cartesian closed: 'CategoryTheory.CartesianClosed'
Cartesian closed: 'CategoryTheory.MonoidalClosed'
abelian category: 'CategoryTheory.Abelian'

Numbers:
Expand Down Expand Up @@ -129,7 +129,7 @@ General algebra:
splitting field: 'Polynomial.SplittingField'
perfect closure: 'PerfectClosure'
Galois correspondence: 'IsGalois.intermediateFieldEquivSubgroup'
Abel-Ruffini theorem (one direction): 'solvableByRad.isSolvable'
Abel-Ruffini theorem (one direction): 'isSolvable_gal_minpoly'

Homological algebra:
chain complex: 'ChainComplex'
Expand All @@ -146,7 +146,7 @@ General algebra:
Chevalley-Warning theorem: 'char_dvd_card_solutions'
"Hensel's lemma (for $\\mathbb{Z}_p$)": 'hensels_lemma'
ring of Witt vectors: 'WittVector'
perfection of a ring: 'Ring.Perfection'
perfection of a ring: 'Perfection'
Transcendental numbers:
Liouville's theorem on existence of transcendental numbers: 'transcendental_liouvilleNumber'

Expand Down Expand Up @@ -200,7 +200,7 @@ Linear algebra:
bilinear form: 'LinearMap.BilinForm'
alternating bilinear form: 'LinearMap.BilinForm.IsAlt'
symmetric bilinear form: 'LinearMap.BilinForm.IsSymm'
matrix representation: 'BilinForm.toMatrix'
matrix representation: 'LinearMap.BilinForm.toMatrix'
quadratic form: 'QuadraticForm'
polar form of a quadratic: 'QuadraticMap.polar'
Finite-dimensional inner product spaces (see also Hilbert spaces, below):
Expand Down Expand Up @@ -366,7 +366,7 @@ Analysis:
principle of isolated zeros: 'AnalyticAt.eventually_eq_zero_or_eventually_ne_zero'
principle of analytic continuation: 'AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq'
analyticity of holomorphic functions: 'DifferentiableOn.analyticAt'
Schwarz lemma: 'Complex.norm_le_norm_of_mapsTo_ball_self'
Schwarz lemma: 'Complex.norm_le_norm_of_mapsTo_ball'
removable singularity: 'Complex.differentiableOn_update_limUnder_insert_of_isLittleO'
Phragmen-Lindelöf principle: 'PhragmenLindelof.horizontal_strip'
fundamental theorem of algebra: 'Complex.isAlgClosed'
Expand Down Expand Up @@ -420,7 +420,7 @@ Probability Theory:
martingale: 'MeasureTheory.Martingale'
optional stopping theorem: 'MeasureTheory.submartingale_iff_expected_stoppedValue_mono'
stopping time: 'MeasureTheory.IsStoppingTime'
hitting time: 'MeasureTheory.hitting'
hitting time: 'MeasureTheory.hittingBtwn'
Gaussian processes: 'ProbabilityTheory.IsGaussianProcess'

Geometry:
Expand Down
8 changes: 4 additions & 4 deletions docs/undergrad.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,8 +197,8 @@ Bilinear and Quadratic Forms Over a Vector Space:
alternating bilinear forms: 'LinearMap.BilinForm.IsAlt'
symmetric bilinear forms: 'LinearMap.BilinForm.IsSymm'
nondegenerate forms: 'LinearMap.BilinForm.Nondegenerate'
matrix representation: 'BilinForm.toMatrix'
change of coordinates: 'BilinForm.toMatrix_comp'
matrix representation: 'LinearMap.BilinForm.toMatrix'
change of coordinates: 'LinearMap.BilinForm.toMatrix_comp'
rank of a bilinear form: ''
Quadratic forms:
quadratic form: 'QuadraticForm'
Expand Down Expand Up @@ -618,8 +618,8 @@ Distribution calculus:
$L^p$ functions: 'MeasureTheory.Lp.toTemperedDistributionCLM'
periodic functions: ''
Dirac comb: ''
Fourier transforms: 'TemperedDistribution.fourierTransformCLM'
inverse Fourier transform: 'TemperedDistribution.fourierTransformInvCLM'
Fourier transforms: 'FourierTransform.fourierCLM'
inverse Fourier transform: 'FourierTransform.fourierInvCLM'
Fourier transform and derivation: ''
Fourier transform and convolution product: ''
Applications:
Expand Down
Loading