Merge remote-tracking branch 'origin/master' into eric-wieser/slash_a…

…ction.redo
leanprover-community · May 4, 2023 · 25af56d · 25af56d
2 parents 51ed55e + 738054f
commit 25af56d
Show file tree

Hide file tree

Showing 115 changed files with 1,728 additions and 1,283 deletions.
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
@@ -216,7 +216,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
     dual isomorphism in the euclidean case: 'inner_product_space.to_dual'
     orthogonal complement: 'submodule.orthogonal'
     Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
-    norm: 'inner_product_space.of_core.to_has_norm'
+    norm: 'inner_product_space.core.to_has_norm'
     orthonormal bases: 'maximal_orthonormal_iff_basis_of_finite_dimensional'
   Endomorphisms:
     orthogonal group: 'matrix.orthogonal_group'

diff --git a/src/algebra/big_operators/fin.lean b/src/algebra/big_operators/fin.lean
@@ -208,6 +208,40 @@ begin
     assoc_rw [hi, inv_mul_cancel_left] }
 end
 
+/-- Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
+Then if `k < j`, this says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ = gₖ`.
+If `k = j`, it says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ₊₁ = gₖgₖ₊₁`.
+If `k > j`, it says `(g₀g₁...gₖ)⁻¹ * g₀g₁...gₖ₊₁ = gₖ₊₁.`
+Useful for defining group cohomology. -/
+@[to_additive "Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
+Then if `k < j`, this says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ) = gₖ`.
+If `k = j`, it says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ + gₖ₊₁`.
+If `k > j`, it says `-(g₀ + g₁ + ... + gₖ) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ₊₁.`
+Useful for defining group cohomology."]
+lemma inv_partial_prod_mul_eq_contract_nth {G : Type*} [group G]
+  (g : fin (n + 1) → G) (j : fin (n + 1)) (k : fin n) :
+  (partial_prod g (j.succ.succ_above k.cast_succ))⁻¹ * partial_prod g (j.succ_above k).succ
+    = j.contract_nth has_mul.mul g k :=
+begin
+  have := partial_prod_right_inv (1 : G) g,
+  simp only [one_smul, coe_eq_cast_succ] at this,
+  rcases lt_trichotomy (k : ℕ) j with (h|h|h),
+  { rwa [succ_above_below, succ_above_below, this, contract_nth_apply_of_lt],
+    { assumption },
+    { rw [cast_succ_lt_iff_succ_le, succ_le_succ_iff, le_iff_coe_le_coe],
+      exact le_of_lt h }},
+  { rwa [succ_above_below, succ_above_above, partial_prod_succ, cast_succ_fin_succ, ←mul_assoc,
+      this, contract_nth_apply_of_eq],
+    { simpa only [le_iff_coe_le_coe, ←h] },
+    { rw [cast_succ_lt_iff_succ_le, succ_le_succ_iff, le_iff_coe_le_coe],
+      exact le_of_eq h }},
+  { rwa [succ_above_above, succ_above_above, partial_prod_succ, partial_prod_succ,
+      cast_succ_fin_succ, partial_prod_succ, inv_mul_cancel_left, contract_nth_apply_of_gt],
+    { exact le_iff_coe_le_coe.2 (le_of_lt h) },
+    { rw [le_iff_coe_le_coe, coe_succ],
+      exact nat.succ_le_of_lt h }},
+end
+
 end partial_prod
 
 end fin

diff --git a/src/algebra/category/Module/biproducts.lean b/src/algebra/category/Module/biproducts.lean
@@ -5,7 +5,6 @@ Authors: Scott Morrison
 -/
 import algebra.group.pi
 import category_theory.limits.shapes.biproducts
-import algebra.category.Module.limits
 import algebra.category.Module.abelian
 import algebra.homology.short_exact.abelian
 

diff --git a/src/algebra/continued_fractions/basic.lean b/src/algebra/continued_fractions/basic.lean
@@ -8,6 +8,9 @@ import algebra.field.defs
 /-!
 # Basic Definitions/Theorems for Continued Fractions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Summary
 
 We define generalised, simple, and regular continued fractions and functions to evaluate their

diff --git a/src/algebra/continued_fractions/computation/approximation_corollaries.lean b/src/algebra/continued_fractions/computation/approximation_corollaries.lean
@@ -6,7 +6,8 @@ Authors: Kevin Kappelmann
 import algebra.continued_fractions.computation.approximations
 import algebra.continued_fractions.convergents_equiv
 import algebra.order.archimedean
-import topology.algebra.order.field
+import algebra.algebra.basic
+import topology.order.basic
 
 /-!
 # Corollaries From Approximation Lemmas (`algebra.continued_fractions.computation.approximations`)

diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau, Chris Hughes
 import data.finset.order
 import algebra.direct_sum.module
 import ring_theory.free_comm_ring
-import ring_theory.ideal.quotient_operations
+import ring_theory.ideal.quotient
 /-!
 # Direct limit of modules, abelian groups, rings, and fields.
 

diff --git a/src/algebra/order/interval.lean b/src/algebra/order/interval.lean
@@ -15,7 +15,7 @@ import tactic.positivity
 
 This file defines arithmetic operations on intervals and prove their correctness. Note that this is
 full precision operations. The essentials of float operations can be found
-in `data.fp.basic`. We hsve not yet integrated these with the rest of the library.
+in `data.fp.basic`. We have not yet integrated these with the rest of the library.
 -/
 
 open function set

diff --git a/src/algebraic_geometry/Spec.lean b/src/algebraic_geometry/Spec.lean
@@ -5,7 +5,6 @@ Authors: Scott Morrison, Justus Springer
 -/
 import algebraic_geometry.locally_ringed_space
 import algebraic_geometry.structure_sheaf
-import logic.equiv.transfer_instance
 import ring_theory.localization.localization_localization
 import topology.sheaves.sheaf_condition.sites
 import topology.sheaves.functors

diff --git a/src/algebraic_geometry/elliptic_curve/point.lean b/src/algebraic_geometry/elliptic_curve/point.lean
@@ -5,8 +5,6 @@ Authors: David Kurniadi Angdinata
 -/
 
 import algebraic_geometry.elliptic_curve.weierstrass
-import field_theory.galois -- temporary import to enable point notation
-import ring_theory.class_group
 
 /-!
 # The group of nonsingular rational points on a Weierstrass curve over a field

diff --git a/src/algebraic_geometry/locally_ringed_space.lean b/src/algebraic_geometry/locally_ringed_space.lean
@@ -6,7 +6,6 @@ Authors: Johan Commelin
 
 import algebraic_geometry.ringed_space
 import algebraic_geometry.stalks
-import logic.equiv.transfer_instance
 
 /-!
 # The category of locally ringed spaces

diff --git a/src/algebraic_geometry/morphisms/open_immersion.lean b/src/algebraic_geometry/morphisms/open_immersion.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import algebraic_geometry.morphisms.ring_hom_properties
 import topology.local_at_target
+import algebraic_geometry.morphisms.basic
 
 /-!
 

diff --git a/src/algebraic_geometry/open_immersion.lean b/src/algebraic_geometry/open_immersion.lean
@@ -12,7 +12,6 @@ import algebraic_geometry.Scheme
 import category_theory.limits.shapes.strict_initial
 import category_theory.limits.shapes.comm_sq
 import algebra.category.Ring.instances
-import topology.local_at_target
 
 /-!
 # Open immersions of structured spaces

diff --git a/src/analysis/bounded_variation.lean b/src/analysis/bounded_variation.lean
@@ -3,7 +3,6 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import measure_theory.measure.lebesgue
 import analysis.calculus.monotone
 import data.set.function
 import algebra.group.basic

diff --git a/src/analysis/calculus/bump_function_findim.lean b/src/analysis/calculus/bump_function_findim.lean
@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 import analysis.calculus.series
 import analysis.convolution
 import analysis.inner_product_space.euclidean_dist
+import measure_theory.measure.haar_lebesgue
 import data.set.pointwise.support
 
 /-!

diff --git a/src/analysis/complex/basic.lean b/src/analysis/complex/basic.lean
@@ -312,10 +312,7 @@ noncomputable instance : is_R_or_C ℂ :=
   conj_I_ax := by simp only [complex.conj_I, ring_hom.coe_mk],
   norm_sq_eq_def_ax := λ z, by simp only [←complex.norm_sq_eq_abs, ←complex.norm_sq_apply,
     add_monoid_hom.coe_mk, complex.norm_eq_abs],
-  mul_im_I_ax := λ z, by simp only [mul_one, add_monoid_hom.coe_mk, complex.I_im],
-  inv_def_ax := λ z, by simp only [complex.inv_def, complex.norm_sq_eq_abs, complex.coe_algebra_map,
-    complex.of_real_eq_coe, complex.norm_eq_abs],
-  div_I_ax := complex.div_I }
+  mul_im_I_ax := λ z, by simp only [mul_one, add_monoid_hom.coe_mk, complex.I_im] }
 
 lemma _root_.is_R_or_C.re_eq_complex_re : ⇑(is_R_or_C.re : ℂ →+ ℝ) = complex.re := rfl
 lemma _root_.is_R_or_C.im_eq_complex_im : ⇑(is_R_or_C.im : ℂ →+ ℝ) = complex.im := rfl

diff --git a/src/analysis/complex/upper_half_plane/topology.lean b/src/analysis/complex/upper_half_plane/topology.lean
@@ -9,7 +9,6 @@ import analysis.convex.normed
 import analysis.convex.complex
 import analysis.complex.re_im_topology
 import topology.homotopy.contractible
-import geometry.manifold.mfderiv
 import geometry.manifold.cont_mdiff_mfderiv
 
 /-!

diff --git a/src/analysis/constant_speed.lean b/src/analysis/constant_speed.lean
@@ -3,8 +3,6 @@ Copyright (c) 2023 Rémi Bottinelli. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémi Bottinelli
 -/
-import measure_theory.measure.lebesgue
-import analysis.calculus.monotone
 import data.set.function
 import analysis.bounded_variation
 import tactic.swap_var

diff --git a/src/analysis/convex/between.lean b/src/analysis/convex/between.lean
@@ -6,8 +6,8 @@ Authors: Joseph Myers
 import data.set.intervals.group
 import analysis.convex.segment
 import linear_algebra.affine_space.finite_dimensional
-import linear_algebra.affine_space.midpoint_zero
 import tactic.field_simp
+import algebra.char_p.invertible
 
 /-!
 # Betweenness in affine spaces

diff --git a/src/analysis/convex/complex.lean b/src/analysis/convex/complex.lean
@@ -9,6 +9,9 @@ import data.complex.module
 /-!
 # Convexity of half spaces in ℂ
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The open and closed half-spaces in ℂ given by an inequality on either the real or imaginary part
 are all convex over ℝ.
 -/

diff --git a/src/analysis/convex/cone/proper.lean b/src/analysis/convex/cone/proper.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Apurva Nakade All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Apurva Nakade
 -/
-import analysis.inner_product_space.adjoint
+import analysis.convex.cone.basic
 
 /-!
 

diff --git a/src/analysis/convex/intrinsic.lean b/src/analysis/convex/intrinsic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert, Yaël Dillies
 -/
 import analysis.normed_space.add_torsor_bases
-import analysis.normed_space.linear_isometry
 
 /-!
 # Intrinsic frontier and interior

diff --git a/src/analysis/fourier/fourier_transform.lean b/src/analysis/fourier/fourier_transform.lean
@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
 
-import analysis.special_functions.complex.circle
 import measure_theory.group.integration
-import measure_theory.integral.integral_eq_improper
+import measure_theory.measure.haar_of_basis
 
 /-!
 # The Fourier transform

diff --git a/src/analysis/fourier/riemann_lebesgue_lemma.lean b/src/analysis/fourier/riemann_lebesgue_lemma.lean
@@ -5,9 +5,7 @@ Authors: David Loeffler
 -/
 
 import measure_theory.function.continuous_map_dense
-import measure_theory.integral.integral_eq_improper
 import measure_theory.group.integration
-import topology.continuous_function.zero_at_infty
 import analysis.fourier.fourier_transform
 import analysis.inner_product_space.dual
 import topology.metric_space.emetric_paracompact