Skip to content

[Merged by Bors] - chore(Algebra): make invertibleInv an instance#31916

Closed
alreadydone wants to merge 1 commit intoleanprover-community:masterfrom
alreadydone:invertibleInv
Closed

[Merged by Bors] - chore(Algebra): make invertibleInv an instance#31916
alreadydone wants to merge 1 commit intoleanprover-community:masterfrom
alreadydone:invertibleInv

Conversation

@alreadydone
Copy link
Copy Markdown
Contributor

@alreadydone alreadydone commented Nov 21, 2025

Open in Gitpod

@alreadydone alreadydone added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) bench-after-CI labels Nov 21, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 21, 2025

PR summary cf85478f35

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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

@ghost
Copy link
Copy Markdown

ghost commented Nov 21, 2025

!bench

@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 Nov 21, 2025
@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Nov 21, 2025 •
edited
Loading

Benchmark results for f33bfb5 against cf85478 are in! @kckennylau @leanprover-community-mathlib4-bot

@alreadydone alreadydone removed the easy < 20s of review time. See the lifecycle page for guidelines. label Nov 21, 2025
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Nov 21, 2025

Here are the benchmark results for commit f33bfb5.
There were no significant changes against commit cf85478.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 21, 2025

File Instructions %
build -17.303⬝10⁹ (-0.01%)
lint +1.345⬝10⁹ (+0.02%)
Mathlib.CategoryTheory.Comma.Over.Pullback +1.86⬝10⁹ (+2.96%)
4 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.Data.Finset.Filter -1.117⬝10⁹ (-11.21%)
Mathlib.Data.List.InsertIdx -1.126⬝10⁹ (-15.22%)
Mathlib.Order.Filter.Map -1.167⬝10⁹ (-3.40%)
Mathlib.CategoryTheory.Limits.Cones -1.621⬝10⁹ (-1.67%)

CI run Lakeprof report

@alreadydone alreadydone added the easy < 20s of review time. See the lifecycle page for guidelines. label Nov 22, 2025
@ocfnash
Copy link
Copy Markdown
Contributor

ocfnash commented Nov 22, 2025

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Nov 22, 2025
mathlib-bors bot pushed a commit that referenced this pull request Nov 22, 2025
@alreadydone
chore(Algebra): make invertibleInv an instance (#31916)
5dcd49b
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 22, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Algebra): make invertibleInv an instance [Merged by Bors] - chore(Algebra): make invertibleInv an instance Nov 22, 2025
@mathlib-bors mathlib-bors bot closed this Nov 22, 2025
@alreadydone alreadydone deleted the invertibleInv branch November 22, 2025 23:59
alok added a commit to alok/mathlib4 that referenced this pull request Mar 17, 2026
@alok
Merge branch 'master' of https://github.com/leanprover-community/math…
3cf430c 
…lib4

* 'master' of https://github.com/leanprover-community/mathlib4: (3130 commits)
  feat(SetTheory/ZFC): add `ZFSet.card` (leanprover-community#29365)
  feat: grind annotations for `choose_spec` (leanprover-community#31927)
  chore(scripts): update nolints.json (leanprover-community#31975)
  feat(Analysis): cos (n * π) = (-1) ^ n (leanprover-community#31971)
  chore: rename `mul_le_mul_right'` to `mul_le_mul_left` (leanprover-community#30242)
  chore: update Mathlib dependencies 2025-11-22 (leanprover-community#31955)
  feat(MeasureTheory): ae-measurability notation wrt non-standard sigma-algebra (leanprover-community#31910)
  doc: add missing spaces around doc code blocks (leanprover-community#31917)
  chore: update Mathlib dependencies 2025-11-22 (leanprover-community#31945)
  chore: shortcut instance for `Nat` to be mul-torsion-free (leanprover-community#31027)
  doc(Topology/Algebra/Algebra): outdated TODO (leanprover-community#31944)
  feat(EqHaar): add `addHaar_nnreal_smul` (leanprover-community#31922)
  chore(Algebra): make invertibleInv an instance (leanprover-community#31916)
  chore(Algebra): change two statements in CubicDiscriminant (leanprover-community#31912)
  chore(MeasureTheory): mark `map_dirac`  as simp (leanprover-community#31909)
  feat: `LinearOrder` instance for `Empty` (leanprover-community#31889)
  chore: deprecate all remaining modules in `Analysis/NormedSpace` (leanprover-community#31913)
  feat(SimpleGraph): weaker condition for paths in acyclic graphs (leanprover-community#25814)
  chore: do not set `group` when declaring option (leanprover-community#31888)
  chore: clean up more unused `Decidable*` instances in types (leanprover-community#31934)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

easy < 20s of review time. See the lifecycle page for guidelines. 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.

4 participants

@alreadydone @leanprover-radar @leanprover-bot @ocfnash