Skip to content

[Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Hom): Deprecate results#12078

Closed
mans0954 wants to merge 13 commits intomasterfrom
mans0954/BilinearForm-Hom-deprecate
Closed

[Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Hom): Deprecate results#12078
mans0954 wants to merge 13 commits intomasterfrom
mans0954/BilinearForm-Hom-deprecate

Conversation

@mans0954
Copy link
Copy Markdown
Collaborator

@mans0954 mans0954 commented Apr 12, 2024 •
edited
Loading

Following the removal of structure BilinForm from Mathlib (#11278) a number of definitions and results in LinearAlgebra/BilinearForm/Hom are essentially just the identity. This PR deprecates these results.

Open in Gitpod

@mans0954 mans0954 added the WIP Work in progress label Apr 12, 2024
@mans0954 mans0954 added awaiting-review and removed WIP Work in progress labels Apr 12, 2024
@mans0954 mans0954 marked this pull request as ready for review April 12, 2024 19:26
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 18, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 18, 2024
@mans0954 mans0954 mentioned this pull request Apr 19, 2024
Closed
1 task
@dupuisf
Copy link
Copy Markdown
Contributor

dupuisf commented Apr 26, 2024

Thanks!

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 26, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 26, 2024
@mans0954
refactor(LinearAlgebra/BilinearForm/Hom): Deprecate results (#12078)
c38e122 
Following the removal of `structure BilinForm` from Mathlib (#11278) a number of definitions and results in `LinearAlgebra/BilinearForm/Hom` are essentially just the identity. This PR deprecates these results.



Co-authored-by: Christopher Hoskin <[email protected]>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 26, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(LinearAlgebra/BilinearForm/Hom): Deprecate results [Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Hom): Deprecate results Apr 26, 2024
@mathlib-bors mathlib-bors bot closed this Apr 26, 2024
@mathlib-bors mathlib-bors bot deleted the mans0954/BilinearForm-Hom-deprecate branch April 26, 2024 10:41
grunweg
grunweg reviewed Apr 26, 2024
View reviewed changes
Mathlib/LinearAlgebra/BilinearForm/Hom.lean
#align bilin_form.to_lin_hom_aux₁ LinearMap.BilinForm.toLinHomAux₁

/-- Auxiliary definition to define `toLinHom`; see below. -/
@[deprecated]
Copy link
Copy Markdown
Contributor

@grunweg grunweg Apr 26, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

Here is how adding a deprecation date could look like:

Suggested change
@[deprecated]
@[deprecated] -- 2024-04-26

Copy link
Copy Markdown
Collaborator Author

@mans0954 mans0954 Apr 28, 2024

Choose a reason for hiding this comment

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

@grunweg there was some discussion around this here but it didn't appear to reach a definite conclusion.

Is your suggestion that the date should be the date of deprecation, or the date when the result can be deleted from Mathlib?

Copy link
Copy Markdown
Contributor

@grunweg grunweg May 2, 2024

Choose a reason for hiding this comment

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

I would aim for the date of deprecation: a deprecation policy will imply then this can be deleted.

Fair enough; I have started a zulip thread trying to create consensus.

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Apr 26, 2024 •
edited
Loading

Thank you for your work refactoring bilinear forms in mathlib. I see that your PR deprecated a few lemmas, but added no deprecation dates to these declarations. My understanding is that we'd like to add them, so we know when we can remove the deprecated results later. :-)
@mans0954 Do you mind adding a deprecation date to all declarations touched here, in a new PR? See my comment for how this could look.

This was referenced Apr 28, 2024
Closed
Closed
mathlib-bors bot pushed a commit that referenced this pull request Apr 29, 2024
@mans0954
doc(RingTheory/Trace): Remove porting note (#12489)
e9bc163 
`toBilin` was depreciated in #12078. This porting note no longer makes sense.
@mans0954 mans0954 mentioned this pull request Apr 30, 2024
Closed
@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Apr 30, 2024

Thank you for your work refactoring bilinear forms in mathlib. I see that your PR deprecated a few lemmas, but added no deprecation dates to these declarations. My understanding is that we'd like to add them, so we know when we can remove the deprecated results later. :-)
@mans0954 Do you mind adding a deprecation date to all declarations touched here, in a new PR? See my comment for how this could look.

#12547

mathlib-bors bot pushed a commit that referenced this pull request May 5, 2024
@mans0954
chore(LinearAlgebra/BilinearForm): Add missing deprecated dates (#12547)
8470448 
Adds dates to results deprecated in #12132 and #12078.
mathlib-bors bot pushed a commit that referenced this pull request May 5, 2024
@mans0954
chore(LinearAlgebra/BilinearForm): Add missing deprecated dates (#12547)
3f1cbbd 
Adds dates to results deprecated in #12132 and #12078.
mathlib-bors bot pushed a commit that referenced this pull request May 5, 2024
@mans0954
chore(LinearAlgebra/BilinearForm): Add missing deprecated dates (#12547)
f9da50e 
Adds dates to results deprecated in #12132 and #12078.
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@mans0954 @apnelson1
refactor(LinearAlgebra/BilinearForm/Hom): Deprecate results (#12078)
d750d65 
Following the removal of `structure BilinForm` from Mathlib (#11278) a number of definitions and results in `LinearAlgebra/BilinearForm/Hom` are essentially just the identity. This PR deprecates these results.



Co-authored-by: Christopher Hoskin <[email protected]>
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@mans0954 @apnelson1
doc(RingTheory/Trace): Remove porting note (#12489)
40c791f 
`toBilin` was depreciated in #12078. This porting note no longer makes sense.
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@mans0954 @apnelson1
chore(LinearAlgebra/BilinearForm): Add missing deprecated dates (#12547)
e45a3d6 
Adds dates to results deprecated in #12132 and #12078.
callesonne pushed a commit that referenced this pull request May 16, 2024
@mans0954 @callesonne
refactor(LinearAlgebra/BilinearForm/Hom): Deprecate results (#12078)
f18897d 
Following the removal of `structure BilinForm` from Mathlib (#11278) a number of definitions and results in `LinearAlgebra/BilinearForm/Hom` are essentially just the identity. This PR deprecates these results.



Co-authored-by: Christopher Hoskin <[email protected]>
callesonne pushed a commit that referenced this pull request May 16, 2024
@mans0954 @callesonne
doc(RingTheory/Trace): Remove porting note (#12489)
01749f4 
`toBilin` was depreciated in #12078. This porting note no longer makes sense.
callesonne pushed a commit that referenced this pull request May 16, 2024
@mans0954 @callesonne
chore(LinearAlgebra/BilinearForm): Add missing deprecated dates (#12547)
f49fbc6 
Adds dates to results deprecated in #12132 and #12078.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mans0954 @dupuisf @grunweg