Skip to content

Commit 20116f5

Browse files
Pjotr5Pjotr5
authored
Merge branch 'master' into expect_assumption
2 parents c2f582d + c557aff commit 20116f5

288 files changed

Lines changed: 4141 additions & 2059 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/weekly-lints.yml‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
name: Weekly linting report
2+
3+
on:
4+
schedule:
5+
- cron: '0 5 * * 1' # Run at 05:00 UTC every Monday
6+
workflow_dispatch:
7+
8+
env:
9+
TOP_MODULE: Mathlib
10+
11+
jobs:
12+
weekly-lints:
13+
name: Build
14+
runs-on: pr
15+
if: github.repository == 'leanprover-community/mathlib4'
16+
steps:
17+
- name: cleanup
18+
run: |
19+
find . -name . -o -prune -exec rm -rf -- {} +
20+
# Delete all but the 5 most recent toolchains.
21+
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
22+
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
23+
if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then
24+
: # Do nothing on success
25+
else
26+
: # Do nothing on failure, but suppress errors
27+
fi
28+
29+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
30+
with:
31+
ref: master
32+
33+
- name: Configure Lean
34+
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
35+
with:
36+
auto-config: false
37+
use-github-cache: false
38+
use-mathlib-cache: false
39+
reinstall-transient-toolchain: true
40+
41+
- name: add weekly linting option
42+
run: |
43+
# Reset contents of the lakefile, so we don't leave the wrong options enabled.
44+
git checkout HEAD -- lakefile.lean
45+
46+
# we disable checking for backticks inside single quotes with the next line
47+
# shellcheck disable=SC2016
48+
# Enable the linter
49+
sed -i -- '/^ -- '\`'latest_import.yml'\`' uses this comment/{s=^= ⟨`linter.weeklyLintSet, true⟩,\n=}' lakefile.lean
50+
51+
# stage the changes in git so that `git diff` can confirm what changed
52+
git add -u
53+
git diff HEAD #lakefile.lean
54+
55+
printf $'\n\nRunning a test %slake build` to verify, for instance, the absence of import loops\n' $'`'
56+
lake build Mathlib.Init
57+
58+
- name: Add GitHub problem matcher wrapper
59+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
60+
with:
61+
action: add
62+
linters: lean
63+
64+
- name: build mathlib
65+
id: build
66+
continue-on-error: true
67+
run: |
68+
# Use a temporary file to ensure we don't overflow max variable size.
69+
lean_outfile=$(mktemp)
70+
# Show the stdout in the GitHub build logs, while we process it from the file.
71+
(lake build || true) | tee "${lean_outfile}"
72+
73+
# Process output for posting to Zulip
74+
SHA=${{ github.sha }} \
75+
REPO=${{ github.repository }} \
76+
RUN_ID=${{ github.run_id }} \
77+
./scripts/zulip_build_report.sh "${lean_outfile}" > "${GITHUB_OUTPUT}"
78+
79+
- name: Remove GitHub problem matcher wrapper
80+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
81+
with:
82+
action: remove
83+
linters: lean
84+
85+
- name: Post output to Zulip
86+
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
87+
with:
88+
api-key: ${{ secrets.ZULIP_API_KEY }}
89+
email: '[email protected]'
90+
organization-url: 'https://leanprover.zulipchat.com'
91+
to: 'mathlib4'
92+
type: 'stream'
93+
topic: Weekly linting log
94+
content: ${{ steps.build.outputs.zulip-message }}

‎Counterexamples.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import Counterexamples.CliffordAlgebraNotInjective
55
import Counterexamples.Cyclotomic105
66
import Counterexamples.DirectSumIsInternal
77
import Counterexamples.DiscreteTopologyNonDiscreteUniformity
8+
import Counterexamples.EulerSumOfPowers
89
import Counterexamples.GameMultiplication
910
import Counterexamples.Girard
1011
import Counterexamples.HomogeneousPrimeNotPrime

‎Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,7 @@ lemma ball_eq_singleton {n : ℕ} : Metric.ball n ((2 : ℝ) ^ (-n - 1 : ℤ)) =
142142

143143

144144
theorem TopIsDiscrete : DiscreteTopology ℕ := by
145-
apply singletons_open_iff_discrete.mp
145+
apply discreteTopology_iff_isOpen_singleton.mpr
146146
intro
147147
simpa only [← ball_eq_singleton] using isOpen_ball
148148

‎Counterexamples/EulerSumOfPowers.lean‎

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
/-
2+
Copyright (c) 2025 Snir Broshi. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Snir Broshi, Michael Stoll
5+
-/
6+
import Mathlib.NumberTheory.FLT.Three
7+
8+
/-!
9+
# Euler's sum of powers conjecture
10+
11+
Euler's sum of powers conjecture says that at least n nth powers of positive integers
12+
are required to sum to an nth power of a positive integer.
13+
14+
This was an attempt to generalize Fermat's Last Theorem,
15+
which is the special case of summing 2 nth powers.
16+
17+
We demonstrate the connection with FLT, prove that it's true for `n ≤ 3`,
18+
and provide counterexamples for `n = 4` and `n = 5`.
19+
The status of the conjecture for `n ≥ 6` is unknown.
20+
21+
https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjecture
22+
http://euler.free.fr/
23+
24+
## TODO
25+
26+
* Formalize Elkies's construction of infinitely many coprime counterexamples for `n = 4`
27+
https://www.ams.org/journals/mcom/1988-51-184/S0025-5718-1988-0930224-9/S0025-5718-1988-0930224-9.pdf
28+
-/
29+
30+
31+
namespace Counterexample
32+
33+
/-- Euler's sum of powers conjecture over a given semiring with a specific exponent. -/
34+
abbrev SumOfPowersConjectureWith (R : Type*) [Semiring R] (n : ℕ) : Prop :=
35+
∀ (a : List R) (b : R), 2 ≤ a.length → 0 ∉ a → b ≠ 0 →
36+
(a.map (· ^ n)).sum = b ^ n → n ≤ a.length
37+
38+
/-- Euler's sum of powers conjecture over the naturals for a given exponent. -/
39+
abbrev SumOfPowersConjectureFor (n : ℕ) : Prop := SumOfPowersConjectureWith ℕ n
40+
41+
/-- Euler's sum of powers conjecture over the naturals. -/
42+
abbrev SumOfPowersConjecture : Prop := ∀ n, SumOfPowersConjectureFor n
43+
44+
/-- Euler's sum of powers conjecture over a given semiring with a specific exponent implies FLT. -/
45+
theorem fermatLastTheoremWith_of_sumOfPowersConjectureWith (R : Type*) [Semiring R] :
46+
∀ n ≥ 3, SumOfPowersConjectureWith R n → FermatLastTheoremWith R n := by
47+
intro n hn conj a b c ha hb hc hsum
48+
have : n ≤ 2 := conj [a, b] c (by simp) (by simp [ha.symm, hb.symm]) hc (by simpa)
49+
cutsat
50+
51+
/-- Euler's sum of powers conjecture over the naturals implies FLT. -/
52+
theorem fermatLastTheorem_of_sumOfPowersConjecture : SumOfPowersConjecture → FermatLastTheorem :=
53+
fun conj n hn ↦ fermatLastTheoremWith_of_sumOfPowersConjectureWith ℕ n hn <| conj n
54+
55+
/-- For `n = 3`, Euler's sum of powers conjecture over a given semiring is equivalent to FLT. -/
56+
theorem sumOfPowersConjectureWith_three_iff_fermatLastTheoremWith_three (R : Type*) [Semiring R] :
57+
SumOfPowersConjectureWith R 3 ↔ FermatLastTheoremWith R 3 := by
58+
refine ⟨fermatLastTheoremWith_of_sumOfPowersConjectureWith R 3 (by rfl), ?_⟩
59+
intro FLT a b ha ha₀ hb₀ hsum
60+
contrapose! hsum
61+
have ⟨x, y, hxy⟩ := a.length_eq_two.mp <| by cutsat
62+
simp [hxy, FLT x y b (by grind) (by grind) hb₀]
63+
64+
/-- Euler's sum of powers conjecture over the naturals is true for `n ≤ 3`. -/
65+
theorem sumOfPowersConjectureFor_le_three : ∀ n ≤ 3, SumOfPowersConjectureFor n := by
66+
intro n hn
67+
by_cases h3 : n = 3
68+
· exact h3 ▸ (sumOfPowersConjectureWith_three_iff_fermatLastTheoremWith_three _).mpr
69+
fermatLastTheoremThree
70+
cutsat
71+
72+
/-- Given a ring homomorphism from `R` to `S` with no nontrivial zeros,
73+
the conjecture over `S` implies the conjecture over `R`. -/
74+
lemma sumOfPowersConjecture_of_ringHom {R S : Type*} [Semiring R] [Semiring S] {f : R →+* S}
75+
(hf : ∀ x, f x = 0 → x = 0) {n : ℕ} (conj : SumOfPowersConjectureWith S n) :
76+
SumOfPowersConjectureWith R n := by
77+
intro a b ha ha₀ hb hsum
78+
have h : (· ^ n) ∘ f = f ∘ (· ^ n) := by ext; simp
79+
convert conj (a.map f) (f b) ?_ ?_ ?_ (by simp [h, hsum, List.sum_map_hom]) <;> grind
80+
81+
/-- Given an injective ring homomorphism from `R` to `S`,
82+
the conjecture over `S` implies the conjecture over `R`. -/
83+
lemma sumOfPowersConjecture_of_injective {R S : Type*} [Semiring R] [Semiring S] {f : R →+* S}
84+
(hf : Function.Injective f) {n : ℕ} (h : SumOfPowersConjectureWith S n) :
85+
SumOfPowersConjectureWith R n :=
86+
sumOfPowersConjecture_of_ringHom (fun _ _ ↦ hf <| by rwa [map_zero]) h
87+
88+
/--
89+
The first counterexample was found by Leon J. Lander and Thomas R. Parkin in 1966
90+
through a computer search, disproving the conjecture.
91+
https://www.ams.org/journals/bull/1966-72-06/S0002-9904-1966-11654-3/S0002-9904-1966-11654-3.pdf
92+
This is also the smallest counterexample for `n = 5`.
93+
-/
94+
theorem sumOfPowersConjectureFor_five_false : ¬SumOfPowersConjectureFor 5 := by
95+
intro conj
96+
let a := [27, 84, 110, 133]
97+
let b := 144
98+
have : 5 ≤ 4 := conj a b (by simp [a]) (by simp [a]) (by simp) (by decide)
99+
cutsat
100+
101+
/--
102+
The first counterexample for `n = 4` was found by Noam D. Elkies in October 1988:
103+
`a := [2_682_440, 15_365_639, 18_796_760]`, `b := 20_615_673`
104+
https://www.ams.org/journals/mcom/1988-51-184/S0025-5718-1988-0930224-9/S0025-5718-1988-0930224-9.pdf
105+
In this paper, Elkies constructs infinitely many solutions to `a^4 + b^4 + c^4 = d^4` for coprime
106+
`a, b, c, d`, which provide infinitely many coprime counterexamples for the case `n = 4`.
107+
Here we use the smallest counterexample for `n = 4`, which was found a month later by Roger E. Frye
108+
https://ieeexplore.ieee.org/document/74138
109+
-/
110+
theorem sumOfPowersConjectureFor_four_false : ¬SumOfPowersConjectureFor 4 := by
111+
intro conj
112+
let a := [95_800, 217_519, 414_560]
113+
let b := 422_481
114+
have : 4 ≤ 3 := conj a b (by simp [a]) (by simp [a]) (by simp) (by decide)
115+
cutsat
116+
117+
/--
118+
For all `(k, m, n)` we define the Diophantine equation `∑ x_i ^ k = ∑ y_i ^ k`
119+
where `x` and `y` are disjoint with length `m` and `n` respectively.
120+
This is a generalization of the diophantine equation of Euler's sum of powers conjecture.
121+
-/
122+
abbrev ExistsEqualSumsOfLikePowersFor (R : Type*) [Semiring R] (k m n : ℕ) : Prop :=
123+
∃ (x y : List R), (x.length = m) ∧ (y.length = n) ∧ (0 ∉ x) ∧ (0 ∉ y) ∧ (List.Disjoint x y) ∧
124+
(x.map (· ^ k)).sum = (y.map (· ^ k)).sum
125+
126+
/-- Euler's sum of powers conjecture for `k` restricts solutions for `(k, m, 1)`. -/
127+
theorem existsEqualSumsOfLikePowersFor_of_sumOfPowersConjectureWith (R : Type*) [Semiring R]
128+
(k m : ℕ) (hm : 2 ≤ m) :
129+
SumOfPowersConjectureWith R k → ExistsEqualSumsOfLikePowersFor R k m 1 → k ≤ m := by
130+
intro conj ⟨x, y, hx, hy, hx₀, hy₀, hdisj, hsum⟩
131+
simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, add_zero,
132+
List.eq_cons_of_length_one hy] at hsum
133+
exact hx ▸ conj x (y.get ⟨0, _⟩) (by cutsat) hx₀ (by grind) hsum
134+
135+
/--
136+
After the first counterexample was found, Leon J. Lander, Thomas R. Parkin, and John Selfridge
137+
made a similar conjecture that is not amenable to the counterexamples found so far.
138+
The status of this conjecture is unknown.
139+
https://en.wikipedia.org/wiki/Lander,_Parkin,_and_Selfridge_conjecture
140+
https://www.ams.org/journals/mcom/1967-21-099/S0025-5718-1967-0222008-0/S0025-5718-1967-0222008-0.pdf
141+
-/
142+
abbrev LanderParkinSelfridgeConjecture (R : Type*) [Semiring R] (k m n : ℕ) : Prop :=
143+
ExistsEqualSumsOfLikePowersFor R k m n → k ≤ m + n
144+
145+
/-- Euler's sum of powers conjecture for `k` implies the Lander, Parkin, and Selfridge conjecture
146+
for `(k, m, 1)`. -/
147+
theorem LanderParkinSelfridgeConjecture_of_sumOfPowersConjectureWith (R : Type*) [Semiring R]
148+
(k m : ℕ) (hm : 2 ≤ m) :
149+
SumOfPowersConjectureWith R k → LanderParkinSelfridgeConjecture R k m 1 := by
150+
intro conj hsum
151+
have := existsEqualSumsOfLikePowersFor_of_sumOfPowersConjectureWith R k m hm conj hsum
152+
cutsat
153+
154+
end Counterexample

‎Counterexamples/IrrationalPowerOfIrrational.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Copyright (c) 2024 Seewoo Lee. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Seewoo Lee
55
-/
6-
import Mathlib.Data.Real.Irrational
76
import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
7+
import Mathlib.RingTheory.Real.Irrational
88

99
/-
1010
# Irrational power of irrational numbers are not necessarily irrational.

‎Counterexamples/SorgenfreyLine.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -231,8 +231,8 @@ theorem isClosed_of_subset_antidiagonal {s : Set (ℝₗ × ℝₗ)} {c : ℝₗ
231231

232232
open Subtype in
233233
instance (c : ℝₗ) : DiscreteTopology {x : ℝₗ × ℝₗ | x.1 + x.2 = c} :=
234-
forall_open_iff_discrete.1 fun U ↦ isClosed_compl_iff.1 <| isClosed_induced_iff.2
235-
⟨val '' Uᶜ, isClosed_of_subset_antidiagonal <| coe_image_subset _ Uᶜ,
234+
discreteTopology_iff_forall_isClosed.2 fun C ↦ isClosed_induced_iff.2
235+
⟨val '' C, isClosed_of_subset_antidiagonal <| coe_image_subset _ C,
236236
preimage_image_eq _ val_injective⟩
237237

238238
/-- The Sorgenfrey plane `ℝₗ × ℝₗ` is not a normal space. -/

‎Mathlib.lean‎

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -658,6 +658,7 @@ import Mathlib.Algebra.Lie.UniversalEnveloping
658658
import Mathlib.Algebra.Lie.Weights.Basic
659659
import Mathlib.Algebra.Lie.Weights.Cartan
660660
import Mathlib.Algebra.Lie.Weights.Chain
661+
import Mathlib.Algebra.Lie.Weights.IsSimple
661662
import Mathlib.Algebra.Lie.Weights.Killing
662663
import Mathlib.Algebra.Lie.Weights.Linear
663664
import Mathlib.Algebra.Lie.Weights.RootSystem
@@ -1679,6 +1680,7 @@ import Mathlib.Analysis.Convex.Uniform
16791680
import Mathlib.Analysis.Convex.Visible
16801681
import Mathlib.Analysis.Convolution
16811682
import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
1683+
import Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
16821684
import Mathlib.Analysis.Distribution.FourierSchwartz
16831685
import Mathlib.Analysis.Distribution.SchwartzSpace
16841686
import Mathlib.Analysis.Fourier.AddCircle
@@ -1706,6 +1708,7 @@ import Mathlib.Analysis.InnerProductSpace.Convex
17061708
import Mathlib.Analysis.InnerProductSpace.Defs
17071709
import Mathlib.Analysis.InnerProductSpace.Dual
17081710
import Mathlib.Analysis.InnerProductSpace.EuclideanDist
1711+
import Mathlib.Analysis.InnerProductSpace.GramMatrix
17091712
import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
17101713
import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
17111714
import Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
@@ -2120,6 +2123,7 @@ import Mathlib.CategoryTheory.Bicategory.End
21202123
import Mathlib.CategoryTheory.Bicategory.EqToHom
21212124
import Mathlib.CategoryTheory.Bicategory.Extension
21222125
import Mathlib.CategoryTheory.Bicategory.Free
2126+
import Mathlib.CategoryTheory.Bicategory.Functor.Cat
21232127
import Mathlib.CategoryTheory.Bicategory.Functor.Lax
21242128
import Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
21252129
import Mathlib.CategoryTheory.Bicategory.Functor.Oplax
@@ -2561,6 +2565,7 @@ import Mathlib.CategoryTheory.Localization.StructuredArrow
25612565
import Mathlib.CategoryTheory.Localization.Triangulated
25622566
import Mathlib.CategoryTheory.Localization.Trifunctor
25632567
import Mathlib.CategoryTheory.LocallyDirected
2568+
import Mathlib.CategoryTheory.MarkovCategory.Basic
25642569
import Mathlib.CategoryTheory.Monad.Adjunction
25652570
import Mathlib.CategoryTheory.Monad.Algebra
25662571
import Mathlib.CategoryTheory.Monad.Basic
@@ -2615,6 +2620,7 @@ import Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
26152620
import Mathlib.CategoryTheory.Monoidal.Free.Basic
26162621
import Mathlib.CategoryTheory.Monoidal.Free.Coherence
26172622
import Mathlib.CategoryTheory.Monoidal.Functor
2623+
import Mathlib.CategoryTheory.Monoidal.Functor.Types
26182624
import Mathlib.CategoryTheory.Monoidal.FunctorCategory
26192625
import Mathlib.CategoryTheory.Monoidal.Grp_
26202626
import Mathlib.CategoryTheory.Monoidal.Hopf_
@@ -2722,6 +2728,7 @@ import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
27222728
import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
27232729
import Mathlib.CategoryTheory.Presentable.Basic
27242730
import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
2731+
import Mathlib.CategoryTheory.Presentable.ColimitPresentation
27252732
import Mathlib.CategoryTheory.Presentable.Finite
27262733
import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
27272734
import Mathlib.CategoryTheory.Presentable.Limits
@@ -2882,6 +2889,7 @@ import Mathlib.CategoryTheory.Triangulated.TriangleShift
28822889
import Mathlib.CategoryTheory.Triangulated.Triangulated
28832890
import Mathlib.CategoryTheory.Triangulated.Yoneda
28842891
import Mathlib.CategoryTheory.Types.Basic
2892+
import Mathlib.CategoryTheory.Types.Monomorphisms
28852893
import Mathlib.CategoryTheory.Types.Set
28862894
import Mathlib.CategoryTheory.UnivLE
28872895
import Mathlib.CategoryTheory.Whiskering
@@ -3631,7 +3639,6 @@ import Mathlib.Data.Real.EReal
36313639
import Mathlib.Data.Real.Embedding
36323640
import Mathlib.Data.Real.GoldenRatio
36333641
import Mathlib.Data.Real.Hyperreal
3634-
import Mathlib.Data.Real.Irrational
36353642
import Mathlib.Data.Real.Pi.Bounds
36363643
import Mathlib.Data.Real.Pi.Irrational
36373644
import Mathlib.Data.Real.Pi.Leibniz
@@ -5377,7 +5384,7 @@ import Mathlib.Probability.Martingale.Upcrossing
53775384
import Mathlib.Probability.Moments.Basic
53785385
import Mathlib.Probability.Moments.ComplexMGF
53795386
import Mathlib.Probability.Moments.Covariance
5380-
import Mathlib.Probability.Moments.CovarianceBilin
5387+
import Mathlib.Probability.Moments.CovarianceBilinDual
53815388
import Mathlib.Probability.Moments.IntegrableExpMul
53825389
import Mathlib.Probability.Moments.MGFAnalytic
53835390
import Mathlib.Probability.Moments.SubGaussian
@@ -5583,6 +5590,7 @@ import Mathlib.RingTheory.Grassmannian
55835590
import Mathlib.RingTheory.HahnSeries.Addition
55845591
import Mathlib.RingTheory.HahnSeries.Basic
55855592
import Mathlib.RingTheory.HahnSeries.HEval
5593+
import Mathlib.RingTheory.HahnSeries.HahnEmbedding
55865594
import Mathlib.RingTheory.HahnSeries.Lex
55875595
import Mathlib.RingTheory.HahnSeries.Multiplication
55885596
import Mathlib.RingTheory.HahnSeries.PowerSeries
@@ -5849,6 +5857,7 @@ import Mathlib.RingTheory.PrincipalIdealDomain
58495857
import Mathlib.RingTheory.PrincipalIdealDomainOfPrime
58505858
import Mathlib.RingTheory.QuotSMulTop
58515859
import Mathlib.RingTheory.Radical
5860+
import Mathlib.RingTheory.Real.Irrational
58525861
import Mathlib.RingTheory.ReesAlgebra
58535862
import Mathlib.RingTheory.Regular.Category
58545863
import Mathlib.RingTheory.Regular.Depth

0 commit comments

Comments
 (0)