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.

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

[Merged by Bors] - feat(RingTheory/LaurentSeries): add properties of the X-adic valuation on Laurent series #14418

Closed
wants to merge 31 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
1388474
first commit
faenuccio May 20, 2024
6b3b435
Merge branch 'master' into fae_PR_intValPowerSeries
faenuccio May 23, 2024
945a96e
Merge branch 'master' into fae_PR_intValPowerSeries
faenuccio Jul 1, 2024
8cdbc20
wip
faenuccio Jul 1, 2024
be79ad8
Added results about Adic val on LaurentSeries
faenuccio Jul 3, 2024
d46fd65
Fixed docstrings
faenuccio Jul 3, 2024
a3a23c8
fixed some import
faenuccio Jul 3, 2024
f80e06b
build fix
faenuccio Jul 3, 2024
614daa0
shake
faenuccio Jul 3, 2024
cab9a6d
added authors
faenuccio Jul 3, 2024
b6d524e
fixed simp lemma
faenuccio Jul 3, 2024
a450c17
fixed unused argument
faenuccio Jul 3, 2024
b892321
renamed one lemma
faenuccio Jul 4, 2024
4cbd3ab
checked until l 501
faenuccio Jul 4, 2024
2d5fcbf
addressed reviewer's comments
faenuccio Jul 4, 2024
2d29b2b
removed one coercion-arrow
faenuccio Jul 4, 2024
6fad983
Merge branch 'fae_PR_intValPowerSeries' into fae_PR_valLaurentSeries
faenuccio Jul 4, 2024
00ab28f
done coeff_zero_of_lt_valuation
faenuccio Jul 4, 2024
1daff87
Merge branch 'master' into fae_PR_valLaurentSeries
faenuccio Jul 5, 2024
b4168ce
Merge branch 'master' into fae_PR_valLaurentSeries
faenuccio Jul 8, 2024
88cb0d0
Merge branch 'master' into fae_PR_valLaurentSeries
faenuccio Jul 10, 2024
70db8e6
fixed two deprecated declarations
faenuccio Jul 11, 2024
e23f1ac
added two more results
faenuccio Jul 11, 2024
2048cb2
Merge branch 'master' into fae_PR_valLaurentSeries
faenuccio Jul 11, 2024
119b35f
wip
faenuccio Jul 12, 2024
ec62fc7
fixed until l.627: two lemmas with f and g needed?
faenuccio Jul 17, 2024
b43b7cd
finished polishing
faenuccio Jul 17, 2024
521a059
made linter happy
faenuccio Jul 17, 2024
4ca1b90
Update Mathlib/RingTheory/LaurentSeries.lean
faenuccio Jul 17, 2024
46ed98b
some doc fix
faenuccio Jul 17, 2024
2712d2d
Merge branch 'fae_PR_valLaurentSeries' of https://github.com/leanprov…
faenuccio Jul 17, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update Mathlib/RingTheory/LaurentSeries.lean
faenuccio authored Jul 17, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
commit 4ca1b908155370ab99d1834eea0cde97ed0f4e5c
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/LaurentSeries.lean
Original file line number Diff line number Diff line change
@@ -34,7 +34,7 @@ the underlying `RatFunc.coeAlgHom`.
### About the `X`-Adic valuation:
* The (integral) valuation of a power series is the order of the first non-zero coefficient, see
`intValuation_le_iff_coeff_lt_eq_zero`.
* The valuation of a laurent series is the order of the first non-zero coefficient, see
* The valuation of a Laurent series is the order of the first non-zero coefficient, see
`valuation_le_iff_coeff_lt_eq_zero`.
* Every Laurent series of valuation less than `(1 : ℤₘ₀)` comes from a power series, see
`val_le_one_iff_eq_coe`.
Loading