[Merged by Bors] - feat(LinearAlgebra/Basis/MulOpposite): basis of an opposite space by themathqueen · Pull Request #25949 · leanprover-community/mathlib4

themathqueen · 2025-06-16T09:37:04Z

This adds the definition of Basis.mulOpposite and shows finite-dimensionality and freeness of Hᵐᵒᵖ.

For motivation, see #25951.

github-actions · 2025-06-16T09:38:20Z

PR summary af6fe588fb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.LinearAlgebra.Basis.MulOpposite` (new file)	1237

Declarations diff

+ finrank
+ instance [DivisionRing R] [AddCommGroup H] [Module R H]
+ instance [Semiring R] [AddCommMonoid H] [Module R H]
+ mulOpposite
+ mulOpposite_apply
+ mulOpposite_repr_eq
+ mulOpposite_repr_op
+ rank
+ repr_unop_eq_mulOpposite_repr

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

j-loreaux · 2025-07-03T16:35:59Z

As with the other PR ~~(which should depend on this one by the way)~~ (sorry, the other one isn't marked blocked-by-other-PR for some reason) why do you want this? It seems to have pretty niche applications in my estimation.

themathqueen · 2025-07-12T14:15:29Z

-awaiting-author

themathqueen · 2025-07-12T14:15:50Z

I've added motivation for these PRs here: #25951

themathqueen · 2025-07-20T23:48:22Z

-awaiting-author

j-loreaux

bors d+

mathlib-bors · 2025-07-21T20:51:21Z

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

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

themathqueen · 2025-07-23T09:27:48Z

bors r+

…5949) This adds the definition of `Basis.mulOpposite` and shows finite-dimensionality and freeness of `Hᵐᵒᵖ`. For motivation, see #25951. Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

mathlib-bors · 2025-07-23T10:06:53Z

Build failed (retrying...):

CI Success

…5949) This adds the definition of `Basis.mulOpposite` and shows finite-dimensionality and freeness of `Hᵐᵒᵖ`. For motivation, see #25951. Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

mathlib-bors · 2025-07-23T10:48:24Z

Build failed (retrying...):

CI Success

…5949) This adds the definition of `Basis.mulOpposite` and shows finite-dimensionality and freeness of `Hᵐᵒᵖ`. For motivation, see #25951. Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

mathlib-bors · 2025-07-23T11:00:30Z

Build failed (retrying...):

CI Success

…5949) This adds the definition of `Basis.mulOpposite` and shows finite-dimensionality and freeness of `Hᵐᵒᵖ`. For motivation, see #25951. Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

mathlib-bors · 2025-07-23T11:30:26Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…anprover-community#25949) This adds the definition of `Basis.mulOpposite` and shows finite-dimensionality and freeness of `Hᵐᵒᵖ`. For motivation, see leanprover-community#25951. Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

added Basis.mulOpposite

37771f7

github-actions Bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc) labels Jun 16, 2025

themathqueen added 2 commits June 16, 2025 09:48

doc string

7f67f27

instance name

888d355

themathqueen mentioned this pull request Jun 16, 2025

[Merged by Bors] - feat(Analysis/InnerProductSpace/MulOpposite): defines the inner product on opposite spaces #25951

Closed

1 task

themathqueen added 2 commits June 18, 2025 20:47

fix style

4337078

fix

167887e

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 3, 2025

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 12, 2025

j-loreaux reviewed Jul 20, 2025

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Basis/MulOpposite.lean Outdated

Comment thread Mathlib/LinearAlgebra/Basis/MulOpposite.lean Outdated

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 20, 2025

themathqueen added 2 commits July 20, 2025 23:44

finrank and rank

de00f24

add simp

d2c2e0c

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 20, 2025

fix

e12fb8b

j-loreaux reviewed Jul 21, 2025

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Basis/MulOpposite.lean

Comment thread Mathlib/LinearAlgebra/Basis/MulOpposite.lean Outdated

Comment thread Mathlib/LinearAlgebra/Basis/MulOpposite.lean Outdated

Comment thread Mathlib/LinearAlgebra/Basis/MulOpposite.lean Outdated

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 21, 2025

themathqueen and others added 3 commits July 21, 2025 21:12

Update Mathlib/LinearAlgebra/Basis/MulOpposite.lean

8069788

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

suggested changes

6e52161

Update MulOpposite.lean

3718f5b

mathlib-bors Bot changed the title ~~feat(LinearAlgebra/Basis/MulOpposite): basis of an opposite space~~ [Merged by Bors] - feat(LinearAlgebra/Basis/MulOpposite): basis of an opposite space Jul 23, 2025

mathlib-bors Bot closed this Jul 23, 2025

themathqueen deleted the basis_mulop branch July 23, 2025 11:30

themathqueen restored the basis_mulop branch July 23, 2025 11:32

themathqueen deleted the basis_mulop branch July 23, 2025 11:36

Conversation

themathqueen commented Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary af6fe588fb

Import changes for modified files

Declarations diff

Uh oh!

j-loreaux commented Jul 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

themathqueen commented Jul 12, 2025

Uh oh!

themathqueen commented Jul 12, 2025

Uh oh!

Uh oh!

Uh oh!

themathqueen commented Jul 20, 2025

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors Bot commented Jul 21, 2025

Uh oh!

themathqueen commented Jul 23, 2025

Uh oh!

mathlib-bors Bot commented Jul 23, 2025

Uh oh!

mathlib-bors Bot commented Jul 23, 2025

Uh oh!

mathlib-bors Bot commented Jul 23, 2025

Uh oh!

mathlib-bors Bot commented Jul 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

themathqueen commented Jun 16, 2025 •

edited

Loading

github-actions Bot commented Jun 16, 2025 •

edited

Loading

j-loreaux commented Jul 3, 2025 •

edited

Loading