From 1fb3229c9e47b3bd62d705adc44d8396f60182e6 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Tue, 20 Jun 2023 03:20:54 +0000 Subject: [PATCH] bump to nightly-2023-06-20-03 mathlib commit https://github.com/leanprover-community/mathlib/commit/0723536a0522d24fc2f159a096fb3304bef77472 --- .../Computation/TerminatesIffRat.lean | 5 +++- Mathbin/CategoryTheory/Enriched/Basic.lean | 5 +++- .../Monoidal/Internal/Limits.lean | 5 +++- Mathbin/Data/Finset/Pairwise.lean | 2 ++ Mathbin/Data/Set/Pairwise/Basic.lean | 4 ++++ Mathbin/Data/Set/Pairwise/Lattice.lean | 4 ++++ Mathbin/Data/Set/Prod.lean | 4 ++++ Mathbin/Data/Zmod/Algebra.lean | 13 ++++++++--- Mathbin/FieldTheory/Cardinality.lean | 4 +++- Mathbin/FieldTheory/Finite/GaloisField.lean | 6 ++--- Mathbin/FieldTheory/Finite/Trace.lean | 5 ++-- .../IsAlgClosed/Classification.lean | 23 ++++++++++--------- Mathbin/FieldTheory/KrullTopology.lean | 5 +++- .../ConditionalExpectation/Basic.lean | 5 +++- .../ConditionalExpectation/CondexpL1.lean | 5 +++- .../ConditionalExpectation/CondexpL2.lean | 5 +++- .../ConditionalExpectation/Indicator.lean | 5 +++- .../Function/ConditionalExpectation/Real.lean | 5 +++- .../LegendreSymbol/AddCharacter.lean | 3 ++- .../NumberTheory/LegendreSymbol/Basic.lean | 5 +++- .../LegendreSymbol/QuadraticChar/Basic.lean | 5 +++- Mathbin/Order/SupIndep.lean | 14 +++++++++++ .../Probability/ConditionalExpectation.lean | 5 +++- Mathbin/Probability/Notation.lean | 5 +++- Mathbin/Probability/Process/Adapted.lean | 5 +++- Mathbin/Probability/Process/Filtration.lean | 5 +++- Mathbin/Probability/Process/Stopping.lean | 5 +++- .../Polynomial/Cyclotomic/Expand.lean | 5 +++- Mathbin/RingTheory/WittVector/Frobenius.lean | 3 ++- README.md | 2 +- lake-manifest.json | 8 +++---- lakefile.lean | 4 ++-- upstream-rev | 2 +- 33 files changed, 139 insertions(+), 47 deletions(-) diff --git a/Mathbin/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean b/Mathbin/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean index 801a09f217..ef80db7d79 100644 --- a/Mathbin/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean +++ b/Mathbin/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kevin Kappelmann ! This file was ported from Lean 3 source module algebra.continued_fractions.computation.terminates_iff_rat -! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -15,6 +15,9 @@ import Mathbin.Data.Rat.Floor /-! # Termination of Continued Fraction Computations (`gcf.of`) +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Summary We show that the continued fraction for a value `v`, as defined in `algebra.continued_fractions.computation.basic`, terminates if and only if `v` corresponds to a diff --git a/Mathbin/CategoryTheory/Enriched/Basic.lean b/Mathbin/CategoryTheory/Enriched/Basic.lean index 9181947e25..80cce35d0e 100644 --- a/Mathbin/CategoryTheory/Enriched/Basic.lean +++ b/Mathbin/CategoryTheory/Enriched/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison ! This file was ported from Lean 3 source module category_theory.enriched.basic -! leanprover-community/mathlib commit 95a87616d63b3cb49d3fe678d416fbe9c4217bf4 +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -16,6 +16,9 @@ import Mathbin.Tactic.ApplyFun /-! # Enriched categories +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We set up the basic theory of `V`-enriched categories, for `V` an arbitrary monoidal category. diff --git a/Mathbin/CategoryTheory/Monoidal/Internal/Limits.lean b/Mathbin/CategoryTheory/Monoidal/Internal/Limits.lean index 3a002a6dad..5fc1a231d5 100644 --- a/Mathbin/CategoryTheory/Monoidal/Internal/Limits.lean +++ b/Mathbin/CategoryTheory/Monoidal/Internal/Limits.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison ! This file was ported from Lean 3 source module category_theory.monoidal.internal.limits -! leanprover-community/mathlib commit 12921e9eaa574d0087ae4856860e6dda8690a438 +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -15,6 +15,9 @@ import Mathbin.CategoryTheory.Limits.Preserves.Basic /-! # Limits of monoid objects. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + If `C` has limits, so does `Mon_ C`, and the forgetful functor preserves these limits. (This could potentially replace many individual constructions for concrete categories, diff --git a/Mathbin/Data/Finset/Pairwise.lean b/Mathbin/Data/Finset/Pairwise.lean index 12e7f5ee57..ba9a51d426 100644 --- a/Mathbin/Data/Finset/Pairwise.lean +++ b/Mathbin/Data/Finset/Pairwise.lean @@ -62,10 +62,12 @@ theorem PairwiseDisjoint.image_finset_of_le [DecidableEq ι] {s : Finset ι} {f #align set.pairwise_disjoint.image_finset_of_le Set.PairwiseDisjoint.image_finset_of_le -/ +#print Set.PairwiseDisjoint.attach /- theorem PairwiseDisjoint.attach (hs : (s : Set ι).PairwiseDisjoint f) : (s.attach : Set { x // x ∈ s }).PairwiseDisjoint (f ∘ Subtype.val) := fun i _ j _ hij => hs i.2 j.2 <| mt Subtype.ext_val hij #align set.pairwise_disjoint.attach Set.PairwiseDisjoint.attach +-/ end SemilatticeInf diff --git a/Mathbin/Data/Set/Pairwise/Basic.lean b/Mathbin/Data/Set/Pairwise/Basic.lean index 99934ae532..4a3a3ecff0 100644 --- a/Mathbin/Data/Set/Pairwise/Basic.lean +++ b/Mathbin/Data/Set/Pairwise/Basic.lean @@ -480,6 +480,7 @@ theorem PairwiseDisjoint.elim_set {s : Set ι} {f : ι → Set α} (hs : s.Pairw /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ +#print Set.PairwiseDisjoint.prod /- theorem PairwiseDisjoint.prod {f : ι → Set α} {g : ι' → Set β} (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjoint g) : (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint fun i => f i.1 ×ˢ g i.2 := @@ -487,7 +488,9 @@ theorem PairwiseDisjoint.prod {f : ι → Set α} {g : ι' → Set β} (hs : s.P disjoint_left.2 fun ⟨a, b⟩ ⟨hai, hbi⟩ ⟨haj, hbj⟩ => hij <| Prod.ext (hs.elim_set hi hj _ hai haj) <| ht.elim_set hi' hj' _ hbi hbj #align set.pairwise_disjoint.prod Set.PairwiseDisjoint.prod +-/ +#print Set.pairwiseDisjoint_pi /- theorem pairwiseDisjoint_pi {ι' α : ι → Type _} {s : ∀ i, Set (ι' i)} {f : ∀ i, ι' i → Set (α i)} (hs : ∀ i, (s i).PairwiseDisjoint (f i)) : ((univ : Set ι).pi s).PairwiseDisjoint fun I => (univ : Set ι).pi fun i => f _ (I i) := @@ -497,6 +500,7 @@ theorem pairwiseDisjoint_pi {ι' α : ι → Type _} {s : ∀ i, Set (ι' i)} {f funext fun i => (hs i).elim_set (hI i trivial) (hJ i trivial) (a i) (haI i trivial) (haJ i trivial) #align set.pairwise_disjoint_pi Set.pairwiseDisjoint_pi +-/ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ #print Set.pairwiseDisjoint_image_right_iff /- diff --git a/Mathbin/Data/Set/Pairwise/Lattice.lean b/Mathbin/Data/Set/Pairwise/Lattice.lean index e987b0f005..56a0c44ce1 100644 --- a/Mathbin/Data/Set/Pairwise/Lattice.lean +++ b/Mathbin/Data/Set/Pairwise/Lattice.lean @@ -101,6 +101,7 @@ theorem PairwiseDisjoint.biUnion {s : Set ι'} {g : ι' → Set ι} {f : ι → -/ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ +#print Set.PairwiseDisjoint.prod_left /- /-- If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is pairwise disjoint. Not to be confused with `set.pairwise_disjoint.prod`. -/ theorem PairwiseDisjoint.prod_left {f : ι × ι' → α} @@ -118,6 +119,7 @@ theorem PairwiseDisjoint.prod_left {f : ι × ι' → α} · convert le_iSup₂ i' hi.2; rfl · convert le_iSup₂ j' hj.2; rfl #align set.pairwise_disjoint.prod_left Set.PairwiseDisjoint.prod_left +-/ end CompleteLattice @@ -126,6 +128,7 @@ section Frame variable [Frame α] /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ +#print Set.pairwiseDisjoint_prod_left /- theorem pairwiseDisjoint_prod_left {s : Set ι} {t : Set ι'} {f : ι × ι' → α} : (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint f ↔ (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) ∧ @@ -138,6 +141,7 @@ theorem pairwiseDisjoint_prod_left {s : Set ι} {t : Set ι'} {f : ι × ι' → · exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij) · exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij) #align set.pairwise_disjoint_prod_left Set.pairwiseDisjoint_prod_left +-/ end Frame diff --git a/Mathbin/Data/Set/Prod.lean b/Mathbin/Data/Set/Prod.lean index 2d1ca76878..07551e26f6 100644 --- a/Mathbin/Data/Set/Prod.lean +++ b/Mathbin/Data/Set/Prod.lean @@ -1049,13 +1049,17 @@ section Nonempty variable [∀ i, Nonempty (α i)] +#print Set.pi_eq_empty_iff' /- theorem pi_eq_empty_iff' : s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅ := by simp [pi_eq_empty_iff] #align set.pi_eq_empty_iff' Set.pi_eq_empty_iff' +-/ +#print Set.disjoint_pi /- @[simp] theorem disjoint_pi : Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i) := by simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff'] #align set.disjoint_pi Set.disjoint_pi +-/ end Nonempty diff --git a/Mathbin/Data/Zmod/Algebra.lean b/Mathbin/Data/Zmod/Algebra.lean index d9798ecbb2..a9a548960e 100644 --- a/Mathbin/Data/Zmod/Algebra.lean +++ b/Mathbin/Data/Zmod/Algebra.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin ! This file was ported from Lean 3 source module data.zmod.algebra -! leanprover-community/mathlib commit 290a7ba01fbcab1b64757bdaa270d28f4dcede35 +! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -31,7 +31,9 @@ section variable {n : ℕ} (m : ℕ) [CharP R m] #print ZMod.algebra' /- -/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n` -/ +/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n`. +See note [reducible non-instances]. -/ +@[reducible] def algebra' (h : m ∣ n) : Algebra (ZMod n) R := { ZMod.castHom h R with smul := fun a r => a * r @@ -48,8 +50,13 @@ def algebra' (h : m ∣ n) : Algebra (ZMod n) R := end -instance (p : ℕ) [CharP R p] : Algebra (ZMod p) R := +/-- The `zmod p`-algebra structure on a ring of characteristic `p`. This is not an +instance since it creates a diamond with `algebra.id`. +See note [reducible non-instances]. -/ +@[reducible] +def algebra (p : ℕ) [CharP R p] : Algebra (ZMod p) R := algebra' R p dvd_rfl +#align zmod.algebra ZMod.algebra end ZMod diff --git a/Mathbin/FieldTheory/Cardinality.lean b/Mathbin/FieldTheory/Cardinality.lean index 693c8c49f6..1bf902fa08 100644 --- a/Mathbin/FieldTheory/Cardinality.lean +++ b/Mathbin/FieldTheory/Cardinality.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Rodriguez ! This file was ported from Lean 3 source module field_theory.cardinality -! leanprover-community/mathlib commit 13e18cfa070ea337ea960176414f5ae3a1534aae +! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -42,8 +42,10 @@ universe u /-- A finite field has prime power cardinality. -/ theorem Fintype.isPrimePow_card_of_field {α} [Fintype α] [Field α] : IsPrimePow ‖α‖ := by + -- TODO: `algebra` version of `char_p.exists`, of type `Σ p, algebra (zmod p) α` cases' CharP.exists α with p _ haveI hp := Fact.mk (CharP.char_is_prime α p) + letI : Algebra (ZMod p) α := ZMod.algebra _ _ let b := IsNoetherian.finsetBasis (ZMod p) α rw [Module.card_fintype b, ZMod.card, isPrimePow_pow_iff] · exact hp.1.IsPrimePow diff --git a/Mathbin/FieldTheory/Finite/GaloisField.lean b/Mathbin/FieldTheory/Finite/GaloisField.lean index cf6a19e32f..2468ab1522 100644 --- a/Mathbin/FieldTheory/Finite/GaloisField.lean +++ b/Mathbin/FieldTheory/Finite/GaloisField.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Aaron Anderson, Alex J. Best, Johan Commelin, Eric Rodriguez, Ruben Van de Velde ! This file was ported from Lean 3 source module field_theory.finite.galois_field -! leanprover-community/mathlib commit 4b05d3f4f0601dca8abf99c4ec99187682ed0bba +! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -165,8 +165,6 @@ theorem splits_zMod_x_pow_sub_x : Splits (RingHom.id (ZMod p)) (X ^ p - X) := rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card] #align galois_field.splits_zmod_X_pow_sub_X GaloisField.splits_zMod_x_pow_sub_x -attribute [-instance] ZMod.algebra - /-- A Galois field with exponent 1 is equivalent to `zmod` -/ def equivZmodP : GaloisField p 1 ≃ₐ[ZMod p] ZMod p := let h : (X ^ p ^ 1 : (ZMod p)[X]) = X ^ Fintype.card (ZMod p) := by rw [pow_one, ZMod.card p] @@ -244,6 +242,8 @@ def ringEquivOfCardEq (hKK' : Fintype.card K = Fintype.card K') : K ≃+* K' := all_goals infer_instance rw [← hpp'] at * haveI := fact_iff.2 hp + letI : Algebra (ZMod p) K := ZMod.algebra _ _ + letI : Algebra (ZMod p) K' := ZMod.algebra _ _ exact alg_equiv_of_card_eq p hKK' #align finite_field.ring_equiv_of_card_eq FiniteField.ringEquivOfCardEq diff --git a/Mathbin/FieldTheory/Finite/Trace.lean b/Mathbin/FieldTheory/Finite/Trace.lean index cde379ac3c..05592d2536 100644 --- a/Mathbin/FieldTheory/Finite/Trace.lean +++ b/Mathbin/FieldTheory/Finite/Trace.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Stoll ! This file was ported from Lean 3 source module field_theory.finite.trace -! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a +! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -25,7 +25,8 @@ finite field, trace namespace FiniteField /-- The trace map from a finite field to its prime field is nongedenerate. -/ -theorem trace_to_zMod_nondegenerate (F : Type _) [Field F] [Finite F] {a : F} (ha : a ≠ 0) : +theorem trace_to_zMod_nondegenerate (F : Type _) [Field F] [Finite F] + [Algebra (ZMod (ringChar F)) F] {a : F} (ha : a ≠ 0) : ∃ b : F, Algebra.trace (ZMod (ringChar F)) F (a * b) ≠ 0 := by haveI : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩ diff --git a/Mathbin/FieldTheory/IsAlgClosed/Classification.lean b/Mathbin/FieldTheory/IsAlgClosed/Classification.lean index 4e8400a623..c6c9570ed7 100644 --- a/Mathbin/FieldTheory/IsAlgClosed/Classification.lean +++ b/Mathbin/FieldTheory/IsAlgClosed/Classification.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes ! This file was ported from Lean 3 source module field_theory.is_alg_closed.classification -! leanprover-community/mathlib commit 660b3a2db3522fa0db036e569dc995a615c4c848 +! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -196,10 +196,9 @@ variable {K L : Type} [Field K] [Field L] [IsAlgClosed K] [IsAlgClosed L] #print IsAlgClosed.ringEquivOfCardinalEqOfCharZero /- /-- Two uncountable algebraically closed fields of characteristic zero are isomorphic if they have the same cardinality. -/ -@[nolint def_lemma] theorem ringEquivOfCardinalEqOfCharZero [CharZero K] [CharZero L] (hK : ℵ₀ < (#K)) - (hKL : (#K) = (#L)) : K ≃+* L := by - apply Classical.choice + (hKL : (#K) = (#L)) : Nonempty (K ≃+* L) := + by cases' exists_isTranscendenceBasis ℤ (show Function.Injective (algebraMap ℤ K) from Int.cast_injective) with @@ -219,9 +218,10 @@ theorem ringEquivOfCardinalEqOfCharZero [CharZero K] [CharZero L] (hK : ℵ₀ < -/ private theorem ring_equiv_of_cardinal_eq_of_char_p (p : ℕ) [Fact p.Prime] [CharP K p] [CharP L p] - (hK : ℵ₀ < (#K)) (hKL : (#K) = (#L)) : K ≃+* L := + (hK : ℵ₀ < (#K)) (hKL : (#K) = (#L)) : Nonempty (K ≃+* L) := by - apply Classical.choice + letI : Algebra (ZMod p) K := ZMod.algebra _ _ + letI : Algebra (ZMod p) L := ZMod.algebra _ _ cases' exists_isTranscendenceBasis (ZMod p) (show Function.Injective (algebraMap (ZMod p) K) from RingHom.injective _) with @@ -246,18 +246,19 @@ private theorem ring_equiv_of_cardinal_eq_of_char_p (p : ℕ) [Fact p.Prime] [Ch #print IsAlgClosed.ringEquivOfCardinalEqOfCharEq /- /-- Two uncountable algebraically closed fields are isomorphic if they have the same cardinality and the same characteristic. -/ -@[nolint def_lemma] theorem ringEquivOfCardinalEqOfCharEq (p : ℕ) [CharP K p] [CharP L p] (hK : ℵ₀ < (#K)) - (hKL : (#K) = (#L)) : K ≃+* L := by - apply Classical.choice + (hKL : (#K) = (#L)) : Nonempty (K ≃+* L) := + by rcases CharP.char_is_prime_or_zero K p with (hp | hp) · haveI : Fact p.prime := ⟨hp⟩ - exact ⟨ring_equiv_of_cardinal_eq_of_char_p p hK hKL⟩ + letI : Algebra (ZMod p) K := ZMod.algebra _ _ + letI : Algebra (ZMod p) L := ZMod.algebra _ _ + exact ring_equiv_of_cardinal_eq_of_char_p p hK hKL · rw [hp] at * skip letI : CharZero K := CharP.charP_to_charZero K letI : CharZero L := CharP.charP_to_charZero L - exact ⟨ring_equiv_of_cardinal_eq_of_char_zero hK hKL⟩ + exact ring_equiv_of_cardinal_eq_of_char_zero hK hKL #align is_alg_closed.ring_equiv_of_cardinal_eq_of_char_eq IsAlgClosed.ringEquivOfCardinalEqOfCharEq -/ diff --git a/Mathbin/FieldTheory/KrullTopology.lean b/Mathbin/FieldTheory/KrullTopology.lean index 635d292155..7a97a81b61 100644 --- a/Mathbin/FieldTheory/KrullTopology.lean +++ b/Mathbin/FieldTheory/KrullTopology.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Monnet ! This file was ported from Lean 3 source module field_theory.krull_topology -! leanprover-community/mathlib commit 039a089d2a4b93c761b234f3e5f5aeb752bac60f +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -16,6 +16,9 @@ import Mathbin.Tactic.ByContra /-! # Krull topology +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the Krull topology on `L ≃ₐ[K] L` for an arbitrary field extension `L/K`. In order to do this, we first define a `group_filter_basis` on `L ≃ₐ[K] L`, whose sets are `E.fixing_subgroup` for all intermediate fields `E` with `E/K` finite dimensional. diff --git a/Mathbin/MeasureTheory/Function/ConditionalExpectation/Basic.lean b/Mathbin/MeasureTheory/Function/ConditionalExpectation/Basic.lean index d4d343663e..d593cc2684 100644 --- a/Mathbin/MeasureTheory/Function/ConditionalExpectation/Basic.lean +++ b/Mathbin/MeasureTheory/Function/ConditionalExpectation/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne ! This file was ported from Lean 3 source module measure_theory.function.conditional_expectation.basic -! leanprover-community/mathlib commit d8bbb04e2d2a44596798a9207ceefc0fb236e41e +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -12,6 +12,9 @@ import Mathbin.MeasureTheory.Function.ConditionalExpectation.CondexpL1 /-! # Conditional expectation +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We build the conditional expectation of an integrable function `f` with value in a Banach space with respect to a measure `μ` (defined on a measurable space structure `m0`) and a measurable space structure `m` with `hm : m ≤ m0` (a sub-sigma-algebra). This is an `m`-strongly measurable diff --git a/Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean b/Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean index 6d71bd79b2..1d7e1a088c 100644 --- a/Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean +++ b/Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne ! This file was ported from Lean 3 source module measure_theory.function.conditional_expectation.condexp_L1 -! leanprover-community/mathlib commit d8bbb04e2d2a44596798a9207ceefc0fb236e41e +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -12,6 +12,9 @@ import Mathbin.MeasureTheory.Function.ConditionalExpectation.CondexpL2 /-! # Conditional expectation in L1 +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains two more steps of the construction of the conditional expectation, which is completed in `measure_theory.function.conditional_expectation.basic`. See that file for a description of the full process. diff --git a/Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean b/Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean index 9e71a419af..9cb5fdb584 100644 --- a/Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean +++ b/Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne ! This file was ported from Lean 3 source module measure_theory.function.conditional_expectation.condexp_L2 -! leanprover-community/mathlib commit d8bbb04e2d2a44596798a9207ceefc0fb236e41e +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -13,6 +13,9 @@ import Mathbin.MeasureTheory.Function.ConditionalExpectation.Unique /-! # Conditional expectation in L2 +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains one step of the construction of the conditional expectation, which is completed in `measure_theory.function.conditional_expectation.basic`. See that file for a description of the full process. diff --git a/Mathbin/MeasureTheory/Function/ConditionalExpectation/Indicator.lean b/Mathbin/MeasureTheory/Function/ConditionalExpectation/Indicator.lean index 52bb43a3d8..65f769f6da 100644 --- a/Mathbin/MeasureTheory/Function/ConditionalExpectation/Indicator.lean +++ b/Mathbin/MeasureTheory/Function/ConditionalExpectation/Indicator.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne ! This file was ported from Lean 3 source module measure_theory.function.conditional_expectation.indicator -! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982 +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -14,6 +14,9 @@ import Mathbin.MeasureTheory.Function.ConditionalExpectation.Basic # Conditional expectation of indicator functions +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file proves some results about the conditional expectation of an indicator function and as a corollary, also proves several results about the behaviour of the conditional expectation on a restricted measure. diff --git a/Mathbin/MeasureTheory/Function/ConditionalExpectation/Real.lean b/Mathbin/MeasureTheory/Function/ConditionalExpectation/Real.lean index 50ef6070ac..ca41356a46 100644 --- a/Mathbin/MeasureTheory/Function/ConditionalExpectation/Real.lean +++ b/Mathbin/MeasureTheory/Function/ConditionalExpectation/Real.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne, Kexing Ying ! This file was ported from Lean 3 source module measure_theory.function.conditional_expectation.real -! leanprover-community/mathlib commit b2ff9a3d7a15fd5b0f060b135421d6a89a999c2f +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -16,6 +16,9 @@ import Mathbin.MeasureTheory.Decomposition.RadonNikodym # Conditional expectation of real-valued functions +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file proves some results regarding the conditional expectation of real-valued functions. ## Main results diff --git a/Mathbin/NumberTheory/LegendreSymbol/AddCharacter.lean b/Mathbin/NumberTheory/LegendreSymbol/AddCharacter.lean index acfc9815e4..c6a5795732 100644 --- a/Mathbin/NumberTheory/LegendreSymbol/AddCharacter.lean +++ b/Mathbin/NumberTheory/LegendreSymbol/AddCharacter.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Stoll ! This file was ported from Lean 3 source module number_theory.legendre_symbol.add_character -! leanprover-community/mathlib commit e3f4be1fcb5376c4948d7f095bec45350bfb9d1a +! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -384,6 +384,7 @@ noncomputable def primitiveCharFiniteField (F F' : Type _) [Field F] [Fintype F] · rw [hq] exact fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf) let ψ := primitive_zmod_char pp F' (ne_zero_iff.mp (NeZero.of_not_dvd F' hp₂)) + letI : Algebra (ZMod p) F := ZMod.algebra _ _ let ψ' := ψ.char.comp (Algebra.trace (ZMod p) F).toAddMonoidHom.toMultiplicative have hψ' : is_nontrivial ψ' := by diff --git a/Mathbin/NumberTheory/LegendreSymbol/Basic.lean b/Mathbin/NumberTheory/LegendreSymbol/Basic.lean index efd77ed57f..3b67582ad1 100644 --- a/Mathbin/NumberTheory/LegendreSymbol/Basic.lean +++ b/Mathbin/NumberTheory/LegendreSymbol/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes, Michael Stoll ! This file was ported from Lean 3 source module number_theory.legendre_symbol.basic -! leanprover-community/mathlib commit 5b2fe80501ff327b9109fb09b7cc8c325cd0d7d9 +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -13,6 +13,9 @@ import Mathbin.NumberTheory.LegendreSymbol.QuadraticChar.Basic /-! # Legendre symbol +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains results about Legendre symbols. We define the Legendre symbol $\Bigl(\frac{a}{p}\Bigr)$ as `legendre_sym p a`. diff --git a/Mathbin/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean b/Mathbin/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean index f0044b1124..9a85e88d41 100644 --- a/Mathbin/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean +++ b/Mathbin/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Stoll ! This file was ported from Lean 3 source module number_theory.legendre_symbol.quadratic_char.basic -! leanprover-community/mathlib commit 5b2fe80501ff327b9109fb09b7cc8c325cd0d7d9 +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -15,6 +15,9 @@ import Mathbin.FieldTheory.Finite.Basic /-! # Quadratic characters of finite fields +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the quadratic character on a finite field `F` and proves some basic statements about it. diff --git a/Mathbin/Order/SupIndep.lean b/Mathbin/Order/SupIndep.lean index 60d9e603b7..9d118a45ce 100644 --- a/Mathbin/Order/SupIndep.lean +++ b/Mathbin/Order/SupIndep.lean @@ -101,12 +101,14 @@ theorem SupIndep.pairwiseDisjoint (hs : s.SupIndep f) : (s : Set ι).PairwiseDis #align finset.sup_indep.pairwise_disjoint Finset.SupIndep.pairwiseDisjoint -/ +#print Finset.SupIndep.le_sup_iff /- theorem SupIndep.le_sup_iff (hs : s.SupIndep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ i, f i ≠ ⊥) : f i ≤ t.sup f ↔ i ∈ t := by refine' ⟨fun h => _, le_sup⟩ by_contra hit exact hf i (disjoint_self.1 <| (hs hts hi hit).mono_right h) #align finset.sup_indep.le_sup_iff Finset.SupIndep.le_sup_iff +-/ #print Finset.supIndep_iff_disjoint_erase /- /-- The RHS looks like the definition of `complete_lattice.independent`. -/ @@ -117,6 +119,7 @@ theorem supIndep_iff_disjoint_erase [DecidableEq ι] : #align finset.sup_indep_iff_disjoint_erase Finset.supIndep_iff_disjoint_erase -/ +#print Finset.SupIndep.image /- theorem SupIndep.image [DecidableEq ι] {s : Finset ι'} {g : ι' → ι} (hs : s.SupIndep (f ∘ g)) : (s.image g).SupIndep f := by intro t ht i hi hit @@ -130,7 +133,9 @@ theorem SupIndep.image [DecidableEq ι] {s : Finset ι'} {g : ι' → ι} (hs : obtain ⟨j, hj, rfl⟩ := mem_image.1 (ht hjt) exact mem_image_of_mem _ (mem_erase.2 ⟨ne_of_apply_ne g (ne_of_mem_of_not_mem hjt hit), hj⟩) #align finset.sup_indep.image Finset.SupIndep.image +-/ +#print Finset.supIndep_map /- theorem supIndep_map {s : Finset ι'} {g : ι' ↪ ι} : (s.map g).SupIndep f ↔ s.SupIndep (f ∘ g) := by refine' ⟨fun hs t ht i hi hit => _, fun hs => _⟩ @@ -141,6 +146,7 @@ theorem supIndep_map {s : Finset ι'} {g : ι' ↪ ι} : (s.map g).SupIndep f rw [map_eq_image] exact hs.image #align finset.sup_indep_map Finset.supIndep_map +-/ #print Finset.supIndep_pair /- @[simp] @@ -196,6 +202,7 @@ theorem SupIndep.attach (hs : s.SupIndep f) : s.attach.SupIndep fun a => f a := #align finset.sup_indep.attach Finset.SupIndep.attach -/ +#print Finset.supIndep_attach /- @[simp] theorem supIndep_attach : (s.attach.SupIndep fun a => f a) ↔ s.SupIndep f := by @@ -210,6 +217,7 @@ theorem supIndep_attach : (s.attach.SupIndep fun a => f a) ↔ s.SupIndep f := Subtype.forall, Subtype.coe_mk] exact fun a => forall_congr' fun j => ⟨fun h _ => h, fun h hj => h (ht hj) hj⟩ #align finset.sup_indep_attach Finset.supIndep_attach +-/ end Lattice @@ -249,6 +257,7 @@ theorem SupIndep.biUnion [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset #align finset.sup_indep.bUnion Finset.SupIndep.biUnion -/ +#print Finset.SupIndep.sigma /- /-- Bind operation for `sup_indep`. -/ theorem SupIndep.sigma {β : ι → Type _} {s : Finset ι} {g : ∀ i, Finset (β i)} {f : Sigma β → α} (hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩) @@ -266,7 +275,9 @@ theorem SupIndep.sigma {β : ι → Type _} {s : Finset ι} {g : ∀ i, Finset ( · convert le_sup hi.2 · convert le_sup hj.2 #align finset.sup_indep.sigma Finset.SupIndep.sigma +-/ +#print Finset.SupIndep.product /- theorem SupIndep.product {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} (hs : s.SupIndep fun i => t.sup fun i' => f (i, i')) (ht : t.SupIndep fun i' => s.sup fun i => f (i, i')) : (s.product t).SupIndep f := @@ -285,7 +296,9 @@ theorem SupIndep.product {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} · convert le_sup hi.2 · convert le_sup hj.2 #align finset.sup_indep.product Finset.SupIndep.product +-/ +#print Finset.supIndep_product_iff /- theorem supIndep_product_iff {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} : (s.product t).SupIndep f ↔ (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ @@ -299,6 +312,7 @@ theorem supIndep_product_iff {s : Finset ι} {t : Finset ι'} {f : ι × ι' → · exact h (mk_mem_product hi hi') (mk_mem_product hj hj') (ne_of_apply_ne Prod.fst hij) · exact h (mk_mem_product hi' hi) (mk_mem_product hj' hj) (ne_of_apply_ne Prod.snd hij) #align finset.sup_indep_product_iff Finset.supIndep_product_iff +-/ end DistribLattice diff --git a/Mathbin/Probability/ConditionalExpectation.lean b/Mathbin/Probability/ConditionalExpectation.lean index cc63805ea9..9bd0c26e3b 100644 --- a/Mathbin/Probability/ConditionalExpectation.lean +++ b/Mathbin/Probability/ConditionalExpectation.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kexing Ying ! This file was ported from Lean 3 source module probability.conditional_expectation -! leanprover-community/mathlib commit 2f8347015b12b0864dfaf366ec4909eb70c78740 +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -16,6 +16,9 @@ import Mathbin.MeasureTheory.Function.ConditionalExpectation.Basic # Probabilistic properties of the conditional expectation +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains some properties about the conditional expectation which does not belong in the main conditional expectation file. diff --git a/Mathbin/Probability/Notation.lean b/Mathbin/Probability/Notation.lean index 66478731b5..134e537f53 100644 --- a/Mathbin/Probability/Notation.lean +++ b/Mathbin/Probability/Notation.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne ! This file was ported from Lean 3 source module probability.notation -! leanprover-community/mathlib commit 00abe0695d8767201e6d008afa22393978bb324d +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -13,6 +13,9 @@ import Mathbin.MeasureTheory.Function.ConditionalExpectation.Basic /-! # Notations for probability theory +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the following notations, for functions `X,Y`, measures `P, Q` defined on a measurable space `m0`, and another measurable space structure `m` with `hm : m ≤ m0`, - `P[X] = ∫ a, X a ∂P` diff --git a/Mathbin/Probability/Process/Adapted.lean b/Mathbin/Probability/Process/Adapted.lean index 2836afee54..00133d0f6f 100644 --- a/Mathbin/Probability/Process/Adapted.lean +++ b/Mathbin/Probability/Process/Adapted.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kexing Ying, Rémy Degenne ! This file was ported from Lean 3 source module probability.process.adapted -! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982 +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -14,6 +14,9 @@ import Mathbin.Topology.Instances.Discrete /-! # Adapted and progressively measurable processes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines some standard definition from the theory of stochastic processes including filtrations and stopping times. These definitions are used to model the amount of information at a specific time and are the first step in formalizing stochastic processes. diff --git a/Mathbin/Probability/Process/Filtration.lean b/Mathbin/Probability/Process/Filtration.lean index de12637077..d3f0b22247 100644 --- a/Mathbin/Probability/Process/Filtration.lean +++ b/Mathbin/Probability/Process/Filtration.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kexing Ying, Rémy Degenne ! This file was ported from Lean 3 source module probability.process.filtration -! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982 +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -13,6 +13,9 @@ import Mathbin.MeasureTheory.Function.ConditionalExpectation.Real /-! # Filtrations +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines filtrations of a measurable space and σ-finite filtrations. ## Main definitions diff --git a/Mathbin/Probability/Process/Stopping.lean b/Mathbin/Probability/Process/Stopping.lean index a81e744481..f476b153ed 100644 --- a/Mathbin/Probability/Process/Stopping.lean +++ b/Mathbin/Probability/Process/Stopping.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kexing Ying, Rémy Degenne ! This file was ported from Lean 3 source module probability.process.stopping -! leanprover-community/mathlib commit ba074af83b6cf54c3104e59402b39410ddbd6dca +! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -13,6 +13,9 @@ import Mathbin.Probability.Process.Adapted /-! # Stopping times, stopped processes and stopped values +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Definition and properties of stopping times. ## Main definitions diff --git a/Mathbin/RingTheory/Polynomial/Cyclotomic/Expand.lean b/Mathbin/RingTheory/Polynomial/Cyclotomic/Expand.lean index 2abeb72fe4..1074e8c89f 100644 --- a/Mathbin/RingTheory/Polynomial/Cyclotomic/Expand.lean +++ b/Mathbin/RingTheory/Polynomial/Cyclotomic/Expand.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Riccardo Brasca ! This file was ported from Lean 3 source module ring_theory.polynomial.cyclotomic.expand -! leanprover-community/mathlib commit 2a0ce625dbb0ffbc7d1316597de0b25c1ec75303 +! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -148,6 +148,7 @@ section CharP theorem cyclotomic_mul_prime_eq_pow_of_not_dvd (R : Type _) {p n : ℕ} [hp : Fact (Nat.Prime p)] [Ring R] [CharP R p] (hn : ¬p ∣ n) : cyclotomic (n * p) R = cyclotomic n R ^ (p - 1) := by + letI : Algebra (ZMod p) R := ZMod.algebra _ _ suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1) by rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow] @@ -165,6 +166,7 @@ theorem cyclotomic_mul_prime_eq_pow_of_not_dvd (R : Type _) {p n : ℕ} [hp : Fa theorem cyclotomic_mul_prime_dvd_eq_pow (R : Type _) {p n : ℕ} [hp : Fact (Nat.Prime p)] [Ring R] [CharP R p] (hn : p ∣ n) : cyclotomic (n * p) R = cyclotomic n R ^ p := by + letI : Algebra (ZMod p) R := ZMod.algebra _ _ suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p by rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow] @@ -198,6 +200,7 @@ theorem isRoot_cyclotomic_prime_pow_mul_iff_of_charP {m k p : ℕ} {R : Type _} [IsDomain R] [hp : Fact (Nat.Prime p)] [hchar : CharP R p] {μ : R} [NeZero (m : R)] : (Polynomial.cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m := by + letI : Algebra (ZMod p) R := ZMod.algebra _ _ rcases k.eq_zero_or_pos with (rfl | hk) · rw [pow_zero, one_mul, is_root_cyclotomic_iff] refine' ⟨fun h => _, fun h => _⟩ diff --git a/Mathbin/RingTheory/WittVector/Frobenius.lean b/Mathbin/RingTheory/WittVector/Frobenius.lean index f39eb27bcf..9597bb64f0 100644 --- a/Mathbin/RingTheory/WittVector/Frobenius.lean +++ b/Mathbin/RingTheory/WittVector/Frobenius.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin ! This file was ported from Lean 3 source module ring_theory.witt_vector.frobenius -! leanprover-community/mathlib commit 2196ab363eb097c008d4497125e0dde23fb36db2 +! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -308,6 +308,7 @@ variable [CharP R p] theorem coeff_frobenius_charP (x : 𝕎 R) (n : ℕ) : coeff (frobenius x) n = x.coeff n ^ p := by rw [coeff_frobenius] + letI : Algebra (ZMod p) R := ZMod.algebra _ _ -- outline of the calculation, proofs follow below calc aeval (fun k => x.coeff k) (frobenius_poly p n) = diff --git a/README.md b/README.md index d4355ebc6f..580b9b8918 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -Tracking mathlib commit: [`2a0ce625dbb0ffbc7d1316597de0b25c1ec75303`](https://github.com/leanprover-community/mathlib/commit/2a0ce625dbb0ffbc7d1316597de0b25c1ec75303) +Tracking mathlib commit: [`0723536a0522d24fc2f159a096fb3304bef77472`](https://github.com/leanprover-community/mathlib/commit/0723536a0522d24fc2f159a096fb3304bef77472) You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3. Please run `lake build` first, to download a copy of the generated `.olean` files. diff --git a/lake-manifest.json b/lake-manifest.json index fb8ff72c86..12b674ec4b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -10,15 +10,15 @@ {"git": {"url": "https://github.com/leanprover-community/lean3port.git", "subDir?": null, - "rev": "17ed3adf03e387934bda0c7f4a298a9bf20cfbda", + "rev": "003ad067093d2f4474eadf3d3dc3115be4272c9c", "name": "lean3port", - "inputRev?": "17ed3adf03e387934bda0c7f4a298a9bf20cfbda"}}, + "inputRev?": "003ad067093d2f4474eadf3d3dc3115be4272c9c"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "5f2c0b7475d9b4d5a792adc2dc7b799d044819ae", + "rev": "e266a22ff12ade06fd8321e1ee806dc7e6a475e5", "name": "mathlib", - "inputRev?": "5f2c0b7475d9b4d5a792adc2dc7b799d044819ae"}}, + "inputRev?": "e266a22ff12ade06fd8321e1ee806dc7e6a475e5"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index f8ec9d2378..9c6397309c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,7 +4,7 @@ open Lake DSL System -- Usually the `tag` will be of the form `nightly-2021-11-22`. -- If you would like to use an artifact from a PR build, -- it will be of the form `pr-branchname-sha`. -def tag : String := "nightly-2023-06-20-01" +def tag : String := "nightly-2023-06-20-03" def releaseRepo : String := "leanprover-community/mathport" def oleanTarName : String := "mathlib3-binport.tar.gz" @@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do untarReleaseArtifact releaseRepo tag oleanTarName libDir return .nil -require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"17ed3adf03e387934bda0c7f4a298a9bf20cfbda" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"003ad067093d2f4474eadf3d3dc3115be4272c9c" @[default_target] lean_lib Mathbin where diff --git a/upstream-rev b/upstream-rev index ac7fd68f08..6378fb7eb1 100644 --- a/upstream-rev +++ b/upstream-rev @@ -1 +1 @@ -2a0ce625dbb0ffbc7d1316597de0b25c1ec75303 +0723536a0522d24fc2f159a096fb3304bef77472