Skip to content

Commit

Permalink
Trigger CI for leanprover/lean4#2766
Browse files Browse the repository at this point in the history
  • Loading branch information
leanprover-community-mathlib4-bot committed Nov 14, 2023
2 parents 6e6d467 + 2a9aeed commit 9e5cdfe
Show file tree
Hide file tree
Showing 260 changed files with 5,696 additions and 4,204 deletions.
2 changes: 2 additions & 0 deletions Archive/Imo/Imo2005Q3.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ Authors: Manuel Candales
-/
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith

#align_import imo.imo2005_q3 from "leanprover-community/mathlib"@"308826471968962c6b59c7ff82a22757386603e3"

Expand Down
3 changes: 3 additions & 0 deletions Archive/Imo/Imo2008Q2.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,9 @@ Authors: Manuel Candales
-/
import Mathlib.Data.Real.Basic
import Mathlib.Data.Set.Finite
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Abel
import Mathlib.Tactic.Linarith

#align_import imo.imo2008_q2 from "leanprover-community/mathlib"@"5f25c089cb34db4db112556f23c50d12da81b297"

Expand Down
2 changes: 1 addition & 1 deletion Archive/Imo/Imo2011Q3.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Renshaw
-/
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Linarith

#align_import imo.imo2011_q3 from "leanprover-community/mathlib"@"5f25c089cb34db4db112556f23c50d12da81b297"

Expand Down Expand Up @@ -57,4 +58,3 @@ theorem imo2011_q3 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) ≤ y * f x + f (f
rw [hno] at hp
linarith
#align imo2011_q3 imo2011_q3

3 changes: 1 addition & 2 deletions Archive/Imo/Imo2013Q5.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Renshaw
-/
import Mathlib.Algebra.GeomSum
import Mathlib.Data.Rat.Defs
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Archimedean
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.LinearCombination

Expand Down
1 change: 1 addition & 0 deletions Archive/Wiedijk100Theorems/CubingACube.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Authors: Floris van Doorn
import Mathlib.Data.Real.Basic
import Mathlib.Data.Set.Finite
import Mathlib.Data.Set.Intervals.Disjoint
import Mathlib.Data.Set.Intervals.Group

#align_import wiedijk_100_theorems.cubing_a_cube from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"

Expand Down
1 change: 1 addition & 0 deletions Archive/Wiedijk100Theorems/InverseTriangleSum.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Authors: Jalex Stark, Yury Kudryashov
-/
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp

#align_import wiedijk_100_theorems.inverse_triangle_sum from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"

Expand Down
2 changes: 1 addition & 1 deletion Archive/ZagierTwoSquares.lean
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ theorem eq_of_mem_fixedPoints {t : zagierSet k} (mem : t ∈ fixedPoints (comple
· -- more
obtain ⟨_, _, _⟩ := mem; simp_all
· -- middle (the one fixed point falls under this case)
simp [zagierSet, Set.mem_setOf_eq] at h
simp only [zagierSet, Set.mem_setOf_eq] at h
replace mem := mem.1
rw [tsub_eq_iff_eq_add_of_le more, ← two_mul] at mem
replace mem := (mul_left_cancel₀ two_ne_zero mem).symm
Expand Down
2 changes: 1 addition & 1 deletion Counterexamples/CliffordAlgebra_not_injective.lean
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ theorem mem_kIdeal_iff (x : MvPolynomial (Fin 3) (ZMod 2)) :
have :
kIdeal = Ideal.span ((monomial · (1 : ZMod 2)) '' Set.range (Finsupp.single · 2)) := by
simp_rw [kIdeal, X, monomial_mul, one_mul, ← Finsupp.single_add, ← Set.range_comp,
Function.comp_def]
Function.comp]
rw [this, mem_ideal_span_monomial_image]
simp

Expand Down
2 changes: 1 addition & 1 deletion Counterexamples/SorgenfreyLine.lean
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ theorem map_toReal_nhds (a : ℝₗ) : map toReal (𝓝 a) = 𝓝[≥] toReal a
#align counterexample.sorgenfrey_line.map_to_real_nhds Counterexample.SorgenfreyLine.map_toReal_nhds

theorem nhds_eq_map (a : ℝₗ) : 𝓝 a = map toReal.symm (𝓝[≥] (toReal a)) := by
simp_rw [← map_toReal_nhds, map_map, Function.comp_def, toReal.symm_apply_apply, map_id']
simp_rw [← map_toReal_nhds, map_map, (· ∘ ·), toReal.symm_apply_apply, map_id']
#align counterexample.sorgenfrey_line.nhds_eq_map Counterexample.SorgenfreyLine.nhds_eq_map

theorem nhds_eq_comap (a : ℝₗ) : 𝓝 a = comap toReal (𝓝[≥] (toReal a)) := by
Expand Down
10 changes: 10 additions & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -803,6 +803,7 @@ import Mathlib.Analysis.NormedSpace.QuaternionExponential
import Mathlib.Analysis.NormedSpace.Ray
import Mathlib.Analysis.NormedSpace.RieszLemma
import Mathlib.Analysis.NormedSpace.Spectrum
import Mathlib.Analysis.NormedSpace.SphereNormEquiv
import Mathlib.Analysis.NormedSpace.Star.Basic
import Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus
import Mathlib.Analysis.NormedSpace.Star.Exponential
Expand Down Expand Up @@ -1228,7 +1229,9 @@ import Mathlib.CategoryTheory.Sites.InducedTopology
import Mathlib.CategoryTheory.Sites.IsSheafFor
import Mathlib.CategoryTheory.Sites.LeftExact
import Mathlib.CategoryTheory.Sites.Limits
import Mathlib.CategoryTheory.Sites.Over
import Mathlib.CategoryTheory.Sites.Plus
import Mathlib.CategoryTheory.Sites.Preserves
import Mathlib.CategoryTheory.Sites.Pretopology
import Mathlib.CategoryTheory.Sites.Pushforward
import Mathlib.CategoryTheory.Sites.RegularExtensive
Expand Down Expand Up @@ -1305,6 +1308,7 @@ import Mathlib.Combinatorics.SetFamily.Intersecting
import Mathlib.Combinatorics.SetFamily.Kleitman
import Mathlib.Combinatorics.SetFamily.LYM
import Mathlib.Combinatorics.SetFamily.Shadow
import Mathlib.Combinatorics.SetFamily.Shatter
import Mathlib.Combinatorics.SimpleGraph.Acyclic
import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
import Mathlib.Combinatorics.SimpleGraph.Basic
Expand Down Expand Up @@ -1400,7 +1404,9 @@ import Mathlib.Data.Buffer.Parser.Numeral
import Mathlib.Data.Bundle
import Mathlib.Data.ByteArray
import Mathlib.Data.Char
import Mathlib.Data.Complex.Abs
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.BigOperators
import Mathlib.Data.Complex.Cardinality
import Mathlib.Data.Complex.Determinant
import Mathlib.Data.Complex.Exponential
Expand Down Expand Up @@ -1833,6 +1839,7 @@ import Mathlib.Data.Rbtree.Init
import Mathlib.Data.Rbtree.Insert
import Mathlib.Data.Rbtree.Main
import Mathlib.Data.Rbtree.MinMax
import Mathlib.Data.Real.Archimedean
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Cardinality
import Mathlib.Data.Real.CauSeq
Expand Down Expand Up @@ -2461,6 +2468,7 @@ import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
import Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
import Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
import Mathlib.MeasureTheory.Constructions.HaarToSphere
import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Constructions.Polish
import Mathlib.MeasureTheory.Constructions.Prod.Basic
Expand Down Expand Up @@ -2584,9 +2592,11 @@ import Mathlib.MeasureTheory.Measure.OuterMeasure
import Mathlib.MeasureTheory.Measure.Portmanteau
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.MeasureTheory.Measure.Regular
import Mathlib.MeasureTheory.Measure.Restrict
import Mathlib.MeasureTheory.Measure.Stieltjes
import Mathlib.MeasureTheory.Measure.Sub
import Mathlib.MeasureTheory.Measure.Trim
import Mathlib.MeasureTheory.Measure.Typeclasses
import Mathlib.MeasureTheory.Measure.VectorMeasure
import Mathlib.MeasureTheory.Measure.WithDensity
import Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure
Expand Down
52 changes: 35 additions & 17 deletions Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
Original file line number Diff line number Diff line change
Expand Up @@ -950,15 +950,21 @@ end NonAssoc

section Center

theorem _root_.Set.smul_mem_center {R A : Type*} [CommSemiring R] [NonUnitalNonAssocSemiring A]
[Module R A] [IsScalarTower R A A] [SMulCommClass R A A](r : R) {a : A}
(ha : a ∈ Set.center A) :
r • a ∈ Set.center A := by
simp [Set.mem_center_iff, mul_smul_comm, smul_mul_assoc, (Set.mem_center_iff A).mp ha]

variable (R A : Type*) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A]
[SMulCommClass R A A]

section NonUnitalNonAssocSemiring
variable {R A : Type*}
variable [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A]
variable [IsScalarTower R A A] [SMulCommClass R A A]

theorem _root_.Set.smul_mem_center (r : R) {a : A} (ha : a ∈ Set.center A) :
r • a ∈ Set.center A where
comm b := by rw [mul_smul_comm, smul_mul_assoc, ha.comm]
left_assoc b c := by rw [smul_mul_assoc, smul_mul_assoc, smul_mul_assoc, ha.left_assoc]
mid_assoc b c := by
rw [mul_smul_comm, smul_mul_assoc, smul_mul_assoc, mul_smul_comm, ha.mid_assoc]
right_assoc b c := by
rw [mul_smul_comm, mul_smul_comm, mul_smul_comm, ha.right_assoc]

variable (R A) in
/-- The center of a non-unital algebra is the set of elements which commute with every element.
They form a non-unital subalgebra. -/
def center : NonUnitalSubalgebra R A :=
Expand All @@ -967,6 +973,14 @@ def center : NonUnitalSubalgebra R A :=
theorem coe_center : (center R A : Set A) = Set.center A :=
rfl

/-- The center of a non-unital algebra is a commutative and associative -/
instance center.instNonUnitalCommSemiring : NonUnitalCommSemiring (center R A) :=
NonUnitalSubsemiring.center.instNonUnitalCommSemiring _

instance center.instNonUnitalCommRing {A : Type*} [NonUnitalNonAssocRing A] [Module R A]
[IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommRing (center R A) :=
NonUnitalSubring.center.instNonUnitalCommRing _

@[simp]
theorem center_toNonUnitalSubsemiring :
(center R A).toNonUnitalSubsemiring = NonUnitalSubsemiring.center A :=
Expand All @@ -977,22 +991,26 @@ theorem center_toNonUnitalSubsemiring :
(center R A).toNonUnitalSubring = NonUnitalSubring.center A :=
rfl

end NonUnitalNonAssocSemiring

variable (R A : Type*) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A]
[SMulCommClass R A A]

-- no instance diamond, as the `npow` field isn't present in the non-unital case.
example :
center.instNonUnitalCommSemiring.toNonUnitalSemiring =
NonUnitalSubsemiringClass.toNonUnitalSemiring (center R A) :=
rfl

@[simp]
theorem center_eq_top (A : Type*) [NonUnitalCommSemiring A] [Module R A] [IsScalarTower R A A]
[SMulCommClass R A A] : center R A = ⊤ :=
SetLike.coe_injective (Set.center_eq_univ A)

variable {R A}

instance center.instNonUnitalCommSemiring : NonUnitalCommSemiring (center R A) :=
NonUnitalSubsemiring.center.instNonUnitalCommSemiring

instance center.instNonUnitalCommRing {A : Type*} [NonUnitalRing A] [Module R A]
[IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommRing (center R A) :=
NonUnitalSubring.center.instNonUnitalCommRing

theorem mem_center_iff {a : A} : a ∈ center R A ↔ ∀ b : A, b * a = a * b :=
Iff.rfl
Subsemigroup.mem_center_iff

end Center

Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1317,7 +1317,7 @@ end Actions
section Center

theorem _root_.Set.algebraMap_mem_center (r : R) : algebraMap R A r ∈ Set.center A := by
simp [Algebra.commutes, Set.mem_center_iff]
simp only [Semigroup.mem_center_iff, commutes, forall_const]
#align set.algebra_map_mem_center Set.algebraMap_mem_center

variable (R A)
Expand Down Expand Up @@ -1357,7 +1357,7 @@ instance {A : Type*} [Ring A] [Algebra R A] : CommRing (center R A) :=
inferInstanceAs (CommRing (Subring.center A))

theorem mem_center_iff {a : A} : a ∈ center R A ↔ ∀ b : A, b * a = a * b :=
Iff.rfl
Subsemigroup.mem_center_iff
#align subalgebra.mem_center_iff Subalgebra.mem_center_iff

end Center
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/BigOperators/Finsupp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -439,7 +439,7 @@ def liftAddHom [AddZeroClass M] [AddCommMonoid N] : (α → M →+ N) ≃+ ((α
right_inv F := by
-- Porting note: This was `ext` and used the wrong lemma
apply Finsupp.addHom_ext'
simp [singleAddHom, AddMonoidHom.comp, comp_def]
simp [singleAddHom, AddMonoidHom.comp, Function.comp]
map_add' F G := by
ext x
exact sum_add
Expand Down
30 changes: 29 additions & 1 deletion Mathlib/Algebra/DirectSum/Decomposition.lean
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,10 @@ submonoids `ℳ i` of that `M`, such that the "recomposition" is canonical. This
works for additive groups and modules.
This is a version of `DirectSum.IsInternal` which comes with a constructive inverse to the
canonical "recomposition" rather than just a proof that the "recomposition" is bijective. -/
canonical "recomposition" rather than just a proof that the "recomposition" is bijective.
Often it is easier to construct a term of this type via `Decomposition.ofAddHom` or
`Decomposition.ofLinearMap`. -/
class Decomposition where
decompose' : M → ⨁ i, ℳ i
left_inv : Function.LeftInverse (DirectSum.coeAddMonoidHom ℳ) decompose'
Expand All @@ -63,6 +66,22 @@ instance : Subsingleton (Decomposition ℳ) :=
congr
exact Function.LeftInverse.eq_rightInverse xr yl⟩

/-- A convenience method to construct a decomposition from an `AddMonoidHom`, such that the proofs
of left and right inverse can be constructed via `ext`. -/
abbrev Decomposition.ofAddHom (decompose : M →+ ⨁ i, ℳ i)
(h_left_inv : (DirectSum.coeAddMonoidHom ℳ).comp decompose = .id _)
(h_right_inv : decompose.comp (DirectSum.coeAddMonoidHom ℳ) = .id _) : Decomposition ℳ where
decompose' := decompose
left_inv := FunLike.congr_fun h_left_inv
right_inv := FunLike.congr_fun h_right_inv

/-- Noncomputably conjure a decomposition instance from a `DirectSum.IsInternal` proof. -/
noncomputable def IsInternal.chooseDecomposition (h : IsInternal ℳ) :
DirectSum.Decomposition ℳ where
decompose' := (Equiv.ofBijective _ h).symm
left_inv := (Equiv.ofBijective _ h).right_inv
right_inv := (Equiv.ofBijective _ h).left_inv

variable [Decomposition ℳ]

protected theorem Decomposition.isInternal : DirectSum.IsInternal ℳ :=
Expand Down Expand Up @@ -230,6 +249,15 @@ variable [DecidableEq ι] [Semiring R] [AddCommMonoid M] [Module R M]

variable (ℳ : ι → Submodule R M)

/-- A convenience method to construct a decomposition from an `LinearMap`, such that the proofs
of left and right inverse can be constructed via `ext`. -/
abbrev Decomposition.ofLinearMap (decompose : M →ₗ[R] ⨁ i, ℳ i)
(h_left_inv : DirectSum.coeLinearMap ℳ ∘ₗ decompose = .id)
(h_right_inv : decompose ∘ₗ DirectSum.coeLinearMap ℳ = .id) : Decomposition ℳ where
decompose' := decompose
left_inv := FunLike.congr_fun h_left_inv
right_inv := FunLike.congr_fun h_right_inv

variable [Decomposition ℳ]

/-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
Expand Down
19 changes: 8 additions & 11 deletions Mathlib/Algebra/Free.lean
Original file line number Diff line number Diff line change
Expand Up @@ -272,11 +272,11 @@ instance : LawfulTraversable FreeMagma.{u} :=
rw [traverse_mul, ih1, ih2, mul_map_seq]
comp_traverse := fun f g x ↦
FreeMagma.recOnPure x
(fun x ↦ by simp only [Function.comp_def, traverse_pure, traverse_pure', functor_norm])
(fun x ↦ by simp only [(· ∘ ·), traverse_pure, traverse_pure', functor_norm])
(fun x y ih1 ih2 ↦ by
rw [traverse_mul, ih1, ih2, traverse_mul];
simp [Functor.Comp.map_mk, Functor.map_map,
Function.comp_def, Comp.seq_mk, seq_map_assoc, map_seq, traverse_mul])
simp [Functor.Comp.map_mk, Functor.map_map, (· ∘ ·), Comp.seq_mk, seq_map_assoc,
map_seq, traverse_mul])
naturality := fun η α β f x ↦
FreeMagma.recOnPure x
(fun x ↦ by simp only [traverse_pure, functor_norm, Function.comp_apply])
Expand Down Expand Up @@ -657,9 +657,8 @@ theorem traverse_mul (x y : FreeSemigroup α) :
List.recOn L1 (fun x ↦ rfl)
(fun hd tl ih x ↦ show
(· * ·) <$> pure <$> F x <*> traverse F (mk hd tl * mk y L2) =
(· * ·) <$> ((· * ·) <$> pure <$> F x <*> traverse F (mk hd tl)) <*> traverse F (mk y L2) by
rw [ih]
simp only [Function.comp_def, (mul_assoc _ _ _).symm, functor_norm])
(· * ·) <$> ((· * ·) <$> pure <$> F x <*> traverse F (mk hd tl)) <*> traverse F (mk y L2)
by rw [ih]; simp only [(· ∘ ·), (mul_assoc _ _ _).symm, functor_norm])
x
#align free_semigroup.traverse_mul FreeSemigroup.traverse_mul

Expand Down Expand Up @@ -688,11 +687,9 @@ instance : LawfulTraversable FreeSemigroup.{u} :=
FreeSemigroup.recOnMul x (fun x ↦ rfl) fun x y ih1 ih2 ↦ by
rw [traverse_mul, ih1, ih2, mul_map_seq]
comp_traverse := fun f g x ↦
recOnPure x (fun x ↦ by
simp only [traverse_pure, functor_norm, Function.comp_def])
fun x y ih1 ih2 ↦ by
rw [traverse_mul, ih1, ih2, traverse_mul, Functor.Comp.map_mk]
simp only [Function.comp_def, functor_norm, traverse_mul]
recOnPure x (fun x ↦ by simp only [traverse_pure, functor_norm, (· ∘ ·)])
fun x y ih1 ih2 ↦ by (rw [traverse_mul, ih1, ih2,
traverse_mul, Functor.Comp.map_mk]; simp only [Function.comp, functor_norm, traverse_mul])
naturality := fun η α β f x ↦
recOnPure x (fun x ↦ by simp only [traverse_pure, functor_norm, Function.comp])
(fun x y ih1 ih2 ↦ by simp only [traverse_mul, functor_norm, ih1, ih2])
Expand Down
5 changes: 2 additions & 3 deletions Mathlib/Algebra/FreeAlgebra.lean
Original file line number Diff line number Diff line change
Expand Up @@ -281,8 +281,7 @@ instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A]
simp only [Algebra.algebraMap_eq_smul_one, smul_eq_mul]
rw [smul_assoc, ←smul_one_mul]

instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A]
[Algebra R A] [Algebra S A] :
instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R A] [Algebra S A] :
SMulCommClass R S (FreeAlgebra A X) where
smul_comm r s x := smul_comm (algebraMap R A r) (algebraMap S A s) x

Expand Down Expand Up @@ -595,7 +594,7 @@ variable {A : Type*} [Semiring A] [Algebra R A]
theorem _root_.Algebra.adjoin_range_eq_range_freeAlgebra_lift (f : X → A) :
Algebra.adjoin R (Set.range f) = (FreeAlgebra.lift R f).range := by
simp only [← Algebra.map_top, ←adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
Function.comp_def, lift_ι_apply]
(· ∘ ·), lift_ι_apply]

/-- Noncommutative version of `Algebra.adjoin_range_eq_range`. -/
theorem _root_.Algebra.adjoin_eq_range_freeAlgebra_lift (s : Set A) :
Expand Down
Loading

0 comments on commit 9e5cdfe

Please sign in to comment.