Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(Mathlib.RingTheory.MvPowerSeries.Evaluation): evaluation of power series #15019

Open
wants to merge 244 commits into
base: master
Choose a base branch
from
Open

feat(Mathlib.RingTheory.MvPowerSeries.Evaluation): evaluation of power series #15019

wants to merge 244 commits into from
+518 −2

Conversation

AntoineChambert-Loir
Copy link
Collaborator

@AntoineChambert-Loir AntoineChambert-Loir commented Jul 22, 2024 •
edited
Loading

AntoineChambert-Loir and others added 30 commits July 18, 2024 13:12
@AntoineChambert-Loir
coefficients of powers of MvPowerSeries
7cb1908
@AntoineChambert-Loir
initial commit
bdef1b0
@AntoineChambert-Loir
update references.bib
06c9528
@AntoineChambert-Loir
delete one blank line
543b97f
@AntoineChambert-Loir
Merge branch 'ACLMIdFF/MvPowerSeries_coeffpow' into ACLMIdFF/MvPowerS…
c2c4976 
…eries_Topology
@AntoineChambert-Loir
defines the topology (removes homogeneous components)
3d5a7d0
@AntoineChambert-Loir
correct def to theorem
2649640
@AntoineChambert-Loir
update
8345665
@AntoineChambert-Loir
mention non-relation with adic topology
805f1d5
@AntoineChambert-Loir
correct centered dots
54bbcea
@AntoineChambert-Loir
update Mathlib.lean
8d001f7
@AntoineChambert-Loir
make lint happy (try to)
d507e68
@AntoineChambert-Loir
update
1191b60
@AntoineChambert-Loir
move weights to other file
cb8c681
@AntoineChambert-Loir
homogeneize
5820cc0
@AntoineChambert-Loir
adjust for degrees
6e26559
@AntoineChambert-Loir
add le_degree
aae13ce
@AntoineChambert-Loir
update mathlib.lean
df1d019
@AntoineChambert-Loir
try to make lint happy
b2bbb36
@AntoineChambert-Loir
adjust
f649884
@AntoineChambert-Loir @faenuccio
Update Mathlib/RingTheory/MvPowerSeries/Basic.lean
4831b9b 
Co-authored-by: Filippo A. E. Nuccio <[email protected]>
@AntoineChambert-Loir @faenuccio
Update Mathlib/RingTheory/MvPowerSeries/Basic.lean
bdfe910 
Co-authored-by: Filippo A. E. Nuccio <[email protected]>
@AntoineChambert-Loir @faenuccio
Update Mathlib/RingTheory/MvPowerSeries/Basic.lean
bafb2d7 
Co-authored-by: Filippo A. E. Nuccio <[email protected]>
@AntoineChambert-Loir @faenuccio
Update Mathlib/RingTheory/MvPowerSeries/Basic.lean
d744b9a 
Co-authored-by: Filippo A. E. Nuccio <[email protected]>
@AntoineChambert-Loir @faenuccio
Update Mathlib/RingTheory/MvPowerSeries/Basic.lean
bc296a4 
Co-authored-by: Filippo A. E. Nuccio <[email protected]>
@AntoineChambert-Loir @faenuccio
Update Mathlib/RingTheory/MvPowerSeries/Basic.lean
93df652 
Co-authored-by: Filippo A. E. Nuccio <[email protected]>
@AntoineChambert-Loir @github-actions
Update Mathlib/RingTheory/MvPowerSeries/Basic.lean
da2b237 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@AntoineChambert-Loir
apply (almost all of) Filippo's comments
c6886c7
@AntoineChambert-Loir
adjust
a2049f3
@AntoineChambert-Loir
adjust and simplify
e7c89bd
@AntoineChambert-Loir AntoineChambert-Loir added the WIP Work in progress label Feb 17, 2025
@AntoineChambert-Loir AntoineChambert-Loir removed the WIP Work in progress label Feb 18, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 19, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Feb 19, 2025
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2025
ADedecker
ADedecker reviewed Mar 4, 2025
View reviewed changes
Copy link
Member

@ADedecker ADedecker left a comment

Choose a reason for hiding this comment

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

I have more comments incoming, but let's start with this.

@ADedecker ADedecker self-assigned this Mar 4, 2025
ADedecker
ADedecker reviewed Mar 5, 2025
View reviewed changes
@ADedecker ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 5, 2025
@AntoineChambert-Loir AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes label Mar 6, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ADedecker ADedecker ADedecker left review comments

Assignees

@ADedecker ADedecker

Labels
t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
Divided Powers
Status: No status
Linear topologies and formal series evaluation
Status: No status
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@AntoineChambert-Loir @mathlib4-dependent-issues-bot @ADedecker @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot @mariainesdff