Skip to content

[Merged by Bors] - feat: add Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits #30085

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

Closed
riccardobrasca wants to merge 17 commits into from
Closed

[Merged by Bors] - feat: add Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits #30085

Changes from 1 commit
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
48a95d6
add file
riccardobrasca Sep 29, 2025
85c6784
useless variables
riccardobrasca Sep 30, 2025
53b4a17
better
riccardobrasca Sep 30, 2025
cd61886
ops
riccardobrasca Sep 30, 2025
cb2b341
Update Mathlib/RingTheory/RootsOfUnity/Units.lean
riccardobrasca Oct 1, 2025
dd9c53e
Update Mathlib/RingTheory/RootsOfUnity/Units.lean
riccardobrasca Oct 1, 2025
987d4a8
Update Mathlib/RingTheory/RootsOfUnity/Units.lean
riccardobrasca Oct 1, 2025
2d002c3
new name
riccardobrasca Oct 5, 2025
5998c0f
add geom_sum_isUnit'
riccardobrasca Oct 5, 2025
1b7a85b
fix name
riccardobrasca Oct 5, 2025
7c3d994
use Set.pairwise
riccardobrasca Oct 5, 2025
c40070d
add ref to pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum
riccardobrasca Oct 5, 2025
a34b92d
Update Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean
riccardobrasca Oct 5, 2025
c12b405
Update Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean
riccardobrasca Oct 5, 2025
6c19e49
Update Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean
riccardobrasca Oct 5, 2025
69e1d86
long line
riccardobrasca Oct 5, 2025
1c61f17
Merge remote-tracking branch 'upstream/master' into RB/cyclot-units
riccardobrasca Oct 5, 2025
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
long line
  • Loading branch information
@riccardobrasca
riccardobrasca committed Oct 5, 2025
commit 69e1d86852cae7a13359ae6a6edae8a4d1e0ec10
3 changes: 2 additions & 1 deletion Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,8 @@ theorem geom_sum_isUnit' (hζ : IsPrimitiveRoot ζ n) (hj : j.Coprime n) (hj_Uni
| 1 => simp_all
| n + 2 => exact geom_sum_isUnit hζ (by linarith) hj

/-- The explicit formula for the unit whose existence is the content of `associated_pow_sub_one_pow_of_coprime`. -/
/-- The explicit formula for the unit whose existence is the content of
`associated_pow_sub_one_pow_of_coprime`. -/
theorem pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum (hζ : IsPrimitiveRoot ζ n)
(hn : 2 ≤ n) : (ζ ^ j - 1) * ∑ k ∈ range i, ζ ^ k = (ζ ^ i - 1) * ∑ k ∈ range j, ζ ^ k := by
apply mul_left_injective₀ (hζ.sub_one_ne_zero (by omega))
Expand Down