Skip to content

[Merged by Bors] - feat: Generalize quadratic isometries to quadratic maps#14719

Closed
eric-wieser wants to merge 7 commits into
masterfrom
eric-wieser/isometry-quadratic-map
Closed

[Merged by Bors] - feat: Generalize quadratic isometries to quadratic maps#14719
eric-wieser wants to merge 7 commits into
masterfrom
eric-wieser/isometry-quadratic-map

Conversation

@eric-wieser

@eric-wieser eric-wieser commented Jul 13, 2024 •
edited
Loading

Copy link
Copy Markdown
Member

Also .prod and .pi, since these are heavily entangled with Isometry and IsometryEquiv.

Follows on from #7569.

Open in Gitpod

@eric-wieser eric-wieser added WIP Work in progress awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Jul 13, 2024
@eric-wieser eric-wieser requested a review from mans0954 July 13, 2024 22:00
@github-actions

github-actions Bot commented Jul 13, 2024 •
edited
Loading

Copy link
Copy Markdown

PR summary 66b58c0d1d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ _root_.QuadraticMap.Isometry.tmul
+ _root_.QuadraticMap.Isometry.tmul_apply
+ instance : Zero ((0 : QuadraticMap R M₁ N) →qᵢ Q₂)
- instance : Zero ((0 : QuadraticForm R M₁) →qᵢ Q₂)
- tmul
- tmul_apply
-+-+ refl

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>

@eric-wieser eric-wieser removed the WIP Work in progress label Jul 13, 2024
@eric-wieser eric-wieser marked this pull request as ready for review July 13, 2024 22:41
@github-actions github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 13, 2024
MichaelStollBayreuth
MichaelStollBayreuth approved these changes Jul 15, 2024
View reviewed changes

@MichaelStollBayreuth MichaelStollBayreuth left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

LGTM!

@MichaelStollBayreuth

MichaelStollBayreuth commented Jul 15, 2024

Copy link
Copy Markdown
Contributor

maintainer merge

@github-actions

github-actions Bot commented Jul 15, 2024

Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

@github-actions github-actions Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 15, 2024
@mattrobball

mattrobball commented Jul 17, 2024

Copy link
Copy Markdown
Contributor

bors merge

@github-actions github-actions Bot added the ready-to-merge This PR has been sent to bors. label Jul 17, 2024
mathlib-bors Bot pushed a commit that referenced this pull request Jul 17, 2024
@eric-wieser
feat: Generalize quadratic isometries to quadratic maps (#14719)
70b6992 
Also `.prod` and `.pi`, since these are heavily entangled with `Isometry` and `IsometryEquiv`.

Follows on from #7569.
@mathlib-bors

mathlib-bors Bot commented Jul 17, 2024

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat: Generalize quadratic isometries to quadratic maps [Merged by Bors] - feat: Generalize quadratic isometries to quadratic maps Jul 17, 2024
@mathlib-bors mathlib-bors Bot closed this Jul 17, 2024
@mathlib-bors mathlib-bors Bot deleted the eric-wieser/isometry-quadratic-map branch July 17, 2024 09:33
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@MichaelStollBayreuth MichaelStollBayreuth MichaelStollBayreuth approved these changes

@mans0954 mans0954 Awaiting requested review from mans0954

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@eric-wieser @MichaelStollBayreuth @mattrobball