Skip to content

[Merged by Bors] - chore (RingTheory/HahnSeries): rm domain hypothesis for invertibility#22284

Closed
ScottCarnahan wants to merge 4 commits intomasterfrom
ScottCarnahan/HahnUnits
Closed

[Merged by Bors] - chore (RingTheory/HahnSeries): rm domain hypothesis for invertibility#22284
ScottCarnahan wants to merge 4 commits intomasterfrom
ScottCarnahan/HahnUnits

Conversation

@ScottCarnahan
Copy link
Copy Markdown
Collaborator

@ScottCarnahan ScottCarnahan commented Feb 25, 2025

This PR refactors some conditions for invertibility of a Hahn series, removing the assumption that the coefficient ring is a domain and that the exponent set is a group.

Open in Gitpod

@ScottCarnahan ScottCarnahan added t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Feb 25, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 25, 2025 •
edited
Loading

PR summary 1830193f16

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ coeff_order_of_eq_add_single
+ isUnit_of_isUnit_leadingCoeff_AddUnitOrder
+ ne_zero_of_eq_add_single
+ one_minus_single_neg_mul
+ order_lt_order_of_eq_add_single
+ order_mul_of_nonzero
+ order_single_mul_of_isRegular

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

jcommelin
jcommelin reviewed Feb 26, 2025
View reviewed changes
Comment thread Mathlib/RingTheory/HahnSeries/Multiplication.lean Outdated
Comment thread Mathlib/RingTheory/HahnSeries/Multiplication.lean Outdated
Comment thread Mathlib/RingTheory/HahnSeries/Multiplication.lean Outdated
jcommelin
jcommelin reviewed Mar 3, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Mar 3, 2025
mathlib-bors bot pushed a commit that referenced this pull request Mar 3, 2025
@ScottCarnahan
chore (RingTheory/HahnSeries): rm domain hypothesis for invertibility (…
96c29c0 
…#22284)

This PR refactors some conditions for invertibility of a Hahn series, removing the assumption that the coefficient ring is a domain and that the exponent set is a group.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 3, 2025

Build failed:

@Parcly-Taxel Parcly-Taxel requested a review from jcommelin March 3, 2025 08:10
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Mar 3, 2025

Network glitch? Let's try again.

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 3, 2025
@ScottCarnahan
chore (RingTheory/HahnSeries): rm domain hypothesis for invertibility (…
7b9802a 
…#22284)

This PR refactors some conditions for invertibility of a Hahn series, removing the assumption that the coefficient ring is a domain and that the exponent set is a group.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 3, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore (RingTheory/HahnSeries): rm domain hypothesis for invertibility [Merged by Bors] - chore (RingTheory/HahnSeries): rm domain hypothesis for invertibility Mar 3, 2025
@mathlib-bors mathlib-bors bot closed this Mar 3, 2025
@mathlib-bors mathlib-bors bot deleted the ScottCarnahan/HahnUnits branch March 3, 2025 11:12
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Jun 3, 2025

This unfortunately got partially reverted in #20594

@eric-wieser eric-wieser mentioned this pull request Jun 3, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Jun 4, 2025
@eric-wieser
fix(HahnSeries): restore a generalization lost in a merge (#25412)
a37ac0b 
This restores a change from #22284 that was accidentally reverted in #20594.

Also avoid using IsAddUnit when the unit can be constructed directly, which gives better defeqs.
joelriou pushed a commit that referenced this pull request Jun 8, 2025
@eric-wieser @joelriou
fix(HahnSeries): restore a generalization lost in a merge (#25412)
f3fec63 
This restores a change from #22284 that was accidentally reverted in #20594.

Also avoid using IsAddUnit when the unit can be constructed directly, which gives better defeqs.
TOMILO87 pushed a commit that referenced this pull request Jun 8, 2025
@eric-wieser @TOMILO87
fix(HahnSeries): restore a generalization lost in a merge (#25412)
17d98cf 
This restores a change from #22284 that was accidentally reverted in #20594.

Also avoid using IsAddUnit when the unit can be constructed directly, which gives better defeqs.
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@eric-wieser @callesonne
fix(HahnSeries): restore a generalization lost in a merge (leanprover…
67edfe6 
…-community#25412)

This restores a change from leanprover-community#22284 that was accidentally reverted in leanprover-community#20594.

Also avoid using IsAddUnit when the unit can be constructed directly, which gives better defeqs.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin Awaiting requested review from jcommelin

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@ScottCarnahan @jcommelin @eric-wieser