Skip to content

[Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents #10432

Closed
mans0954 wants to merge 24 commits intomasterfrom
mans0954/bilinform-symm2
Closed

[Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents #10432
mans0954 wants to merge 24 commits intomasterfrom
mans0954/bilinform-symm2

Conversation

@mans0954
Copy link
Copy Markdown
Collaborator

@mans0954 mans0954 commented Feb 11, 2024 •
edited
Loading

Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap.IsRefl and LinearMap.IsSymm.

Open in Gitpod

@mans0954 mans0954 mentioned this pull request Feb 11, 2024
Closed
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 11, 2024
@mans0954 mans0954 mentioned this pull request Feb 14, 2024
Closed
@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 Feb 26, 2024
@mans0954 mans0954 mentioned this pull request Mar 10, 2024
Closed
1 task
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 19, 2024
@ghost
Copy link
Copy Markdown

ghost commented Mar 19, 2024

This PR/issue depends on:

@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 Mar 19, 2024
@mans0954 mans0954 marked this pull request as ready for review March 19, 2024 07:03
mathlib-bors bot pushed a commit that referenced this pull request Apr 9, 2024
@mans0954 @eric-wieser @Vierkantor
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
aee79f6 
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278)

Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm`

Closes: #10553 

This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs.

Supersedes: 

- #11057
- #11032
- #10432
- #10422



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Vierkantor <[email protected]>
@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 9, 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 9, 2024
@mans0954 mans0954 changed the title refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl and BilinForm.IsSymm in terms of LinearMap equivalents refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents Apr 13, 2024
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@mans0954 @eric-wieser
@Vierkantor @xgenereux
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
e5ec108 
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278)

Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm`

Closes: #10553 

This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs.

Supersedes: 

- #11057
- #11032
- #10432
- #10422



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Vierkantor <[email protected]>
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@mans0954 @eric-wieser
@Vierkantor @atarnoam
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
6db7513 
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278)

Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm`

Closes: #10553 

This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs.

Supersedes: 

- #11057
- #11032
- #10432
- #10422



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Vierkantor <[email protected]>
eric-wieser
eric-wieser reviewed Apr 18, 2024
View reviewed changes
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@mans0954 @eric-wieser
@Vierkantor @uniwuni
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
1ce336b 
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278)

Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm`

Closes: #10553 

This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs.

Supersedes: 

- #11057
- #11032
- #10432
- #10422



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Vierkantor <[email protected]>
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@mans0954 @eric-wieser
@Vierkantor @callesonne
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
9cfef67 
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278)

Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm`

Closes: #10553 

This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs.

Supersedes: 

- #11057
- #11032
- #10432
- #10422



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Vierkantor <[email protected]>
eric-wieser
eric-wieser reviewed Apr 26, 2024
View reviewed changes
@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 26, 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 28, 2024
@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 May 30, 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 Jun 1, 2024
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Jun 1, 2024

bors d+

Sorry for forgetting about this one

Is the description still correct? You already did replace BilinForm, right?

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 1, 2024

✌️ mans0954 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 Jun 1, 2024
@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Jun 1, 2024

Is the description still correct? You already did replace BilinForm, right?

I opened this PR before we did that! I think the PR is still useful for reducing duplication though. I've updated the description. Thanks.

@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Jun 1, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jun 1, 2024
@mans0954 @eric-wieser
refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.I…
5f37a7e 
…sRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents (#10432)

Redefine `BilinForm.IsRefl`, `BilinForm.IsAlt` and `BilinForm.IsSymm` in terms of `LinearMap.IsRefl` and `LinearMap.IsSymm`.



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

mathlib-bors bot commented Jun 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents [Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents Jun 1, 2024
@mathlib-bors mathlib-bors bot closed this Jun 1, 2024
@mathlib-bors mathlib-bors bot deleted the mans0954/bilinform-symm2 branch June 1, 2024 08:18
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@mans0954 @eric-wieser @callesonne
refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.I…
d7fa538 
…sRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents (#10432)

Redefine `BilinForm.IsRefl`, `BilinForm.IsAlt` and `BilinForm.IsSymm` in terms of `LinearMap.IsRefl` and `LinearMap.IsSymm`.



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
grunweg pushed a commit that referenced this pull request Jun 7, 2024
@mans0954 @eric-wieser @grunweg
refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.I…
1974448 
…sRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents (#10432)

Redefine `BilinForm.IsRefl`, `BilinForm.IsAlt` and `BilinForm.IsSymm` in terms of `LinearMap.IsRefl` and `LinearMap.IsSymm`.



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@mans0954 @eric-wieser @AntoineChambert-Loir
refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.I…
3c1dce4 
…sRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents (#10432)

Redefine `BilinForm.IsRefl`, `BilinForm.IsAlt` and `BilinForm.IsSymm` in terms of `LinearMap.IsRefl` and `LinearMap.IsSymm`.



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
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

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.

2 participants

@mans0954 @eric-wieser