bump to nightly-2023-04-14-02

mathlib commit leanprover-community/mathlib@7ebf83e

Mathbin/Analysis/Asymptotics/Asymptotics.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.asymptotics.asymptotics
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 9a48a083b390d9b84a71efbdc4e8dfa26a687104
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Topology.LocalHomeomorph
 /-!
 # Asymptotics
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce these relations:
 
 * `is_O_with c l f g` : "f is big O of g along l with constant c";

Mathbin/Analysis/Convex/Quasiconvex.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module analysis.convex.quasiconvex
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit 9a48a083b390d9b84a71efbdc4e8dfa26a687104
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Analysis.Convex.Function
 /-!
 # Quasiconvex and quasiconcave functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines quasiconvexity, quasiconcavity and quasilinearity of functions, which are
 generalizations of unimodality and monotonicity. Convexity implies quasiconvexity, concavity implies
 quasiconcavity, and monotonicity implies quasilinearity.

Mathbin/Analysis/LocallyConvex/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean Lo, Bhavik Mehta, Yaël Dillies
 
 ! This file was ported from Lean 3 source module analysis.locally_convex.basic
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 9a48a083b390d9b84a71efbdc4e8dfa26a687104
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Analysis.NormedSpace.Basic
 /-!
 # Local convexity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines absorbent and balanced sets.
 
 An absorbent set is one that "surrounds" the origin. The idea is made precise by requiring that any

Mathbin/Analysis/Normed/Order/UpperLower.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module analysis.normed.order.upper_lower
-! leanprover-community/mathlib commit 992efbda6f85a5c9074375d3c7cb9764c64d8f72
+! leanprover-community/mathlib commit 9a48a083b390d9b84a71efbdc4e8dfa26a687104
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Topology.Algebra.Order.UpperLower
 /-!
 # Upper/lower/order-connected sets in normed groups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The topological closure and interior of an upper/lower/order-connected set is an
 upper/lower/order-connected set (with the notable exception of the closure of an order-connected
 set).

Mathbin/Analysis/NormedSpace/ContinuousLinearMap.lean

@@ -4,14 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
 
 ! This file was ported from Lean 3 source module analysis.normed_space.continuous_linear_map
-! leanprover-community/mathlib commit e0e2f10d64d8a5fd11140de398eaa1322eb46c07
+! leanprover-community/mathlib commit 9a48a083b390d9b84a71efbdc4e8dfa26a687104
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Analysis.NormedSpace.Basic
 
 /-! # Constructions of continuous linear maps between (semi-)normed spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A fundamental fact about (semi-)linear maps between normed spaces over sensible fields is that
 continuity and boundedness are equivalent conditions.  That is, for normed spaces `E`, `F`, a
 `linear_map` `f : E →ₛₗ[σ] F` is the coercion of some `continuous_linear_map` `f' : E →SL[σ] F`, if

Mathbin/Analysis/NormedSpace/Ray.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Yaël Dillies
 
 ! This file was ported from Lean 3 source module analysis.normed_space.ray
-! leanprover-community/mathlib commit 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
+! leanprover-community/mathlib commit 9a48a083b390d9b84a71efbdc4e8dfa26a687104
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Analysis.NormedSpace.Basic
 /-!
 # Rays in a real normed vector space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove some lemmas about the `same_ray` predicate in case of a real normed space. In
 this case, for two vectors `x y` in the same ray, the norm of their sum is equal to the sum of their
 norms and `‖y‖ • x = ‖x‖ • y`.

Mathbin/Analysis/NormedSpace/RieszLemma.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean Lo, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.normed_space.riesz_lemma
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 9a48a083b390d9b84a71efbdc4e8dfa26a687104
 ! 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.MetricSpace.HausdorffDistance
 /-!
 # Applications of the Hausdorff distance in normed spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Riesz's lemma, stated for a normed space over a normed field: for any
 closed proper subspace `F` of `E`, there is a nonzero `x` such that `‖x - F‖`
 is at least `r * ‖x‖` for any `r < 1`. This is `riesz_lemma`.

Mathbin/Analysis/Seminorm.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean Lo, Yaël Dillies, Moritz Doll
 
 ! This file was ported from Lean 3 source module analysis.seminorm
-! leanprover-community/mathlib commit 832a8ba8f10f11fea99367c469ff802e69a5b8ec
+! leanprover-community/mathlib commit 7ebf83ed9c262adbf983ef64d5e8c2ae94b625f4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -255,12 +255,22 @@ theorem smul_sup [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] (r
 instance : PartialOrder (Seminorm 𝕜 E) :=
   PartialOrder.lift _ FunLike.coe_injective
 
-theorem le_def (p q : Seminorm 𝕜 E) : p ≤ q ↔ (p : E → ℝ) ≤ q :=
+@[simp, norm_cast]
+theorem coe_le_coe {p q : Seminorm 𝕜 E} : (p : E → ℝ) ≤ q ↔ p ≤ q :=
   Iff.rfl
-#align seminorm.le_def Seminorm.le_def
+#align seminorm.coe_le_coe Seminorm.coe_le_coe
+
+@[simp, norm_cast]
+theorem coe_lt_coe {p q : Seminorm 𝕜 E} : (p : E → ℝ) < q ↔ p < q :=
+  Iff.rfl
+#align seminorm.coe_lt_coe Seminorm.coe_lt_coe
 
-theorem lt_def (p q : Seminorm 𝕜 E) : p < q ↔ (p : E → ℝ) < q :=
+theorem le_def {p q : Seminorm 𝕜 E} : p ≤ q ↔ ∀ x, p x ≤ q x :=
   Iff.rfl
+#align seminorm.le_def Seminorm.le_def
+
+theorem lt_def {p q : Seminorm 𝕜 E} : p < q ↔ p ≤ q ∧ ∃ x, p x < q x :=
+  Pi.lt_def
 #align seminorm.lt_def Seminorm.lt_def
 
 instance : SemilatticeSup (Seminorm 𝕜 E) :=
@@ -364,7 +374,7 @@ theorem bot_eq_zero : (⊥ : Seminorm 𝕜 E) = 0 :=
 
 theorem smul_le_smul {p q : Seminorm 𝕜 E} {a b : ℝ≥0} (hpq : p ≤ q) (hab : a ≤ b) : a • p ≤ b • q :=
   by
-  simp_rw [le_def, Pi.le_def, coe_smul]
+  simp_rw [le_def, coe_smul]
   intro x
   simp_rw [Pi.smul_apply, NNReal.smul_def, smul_eq_mul]
   exact mul_le_mul hab (hpq x) (map_nonneg p x) (NNReal.coe_nonneg b)

Mathbin/CategoryTheory/Idempotents/SimplicialObject.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 
 ! This file was ported from Lean 3 source module category_theory.idempotents.simplicial_object
-! leanprover-community/mathlib commit 163d1a6d98caf9f0431704169027e49c5c6c6cc0
+! leanprover-community/mathlib commit 9a48a083b390d9b84a71efbdc4e8dfa26a687104
 ! 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.Idempotents.FunctorCategories
 
 # Idempotent completeness of categories of simplicial objects
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we provide an instance expressing that `simplicial_object C`
 and `cosimplicial_object C` are idempotent complete categories when the
 category `C` is.

Mathbin/Data/Matrix/Rank.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.matrix.rank
-! leanprover-community/mathlib commit b5b5dd5a47b5744260e2c9185013075ce9dadccd
+! leanprover-community/mathlib commit 86add5ce96b35c2cc6ee6946ab458e7302584e21
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -23,7 +23,7 @@ This definition does not depend on the choice of basis, see `matrix.rank_eq_finr
 
 ## TODO
 
-* Show that `matrix.rank` is equal to the row-rank and column-rank
+* Show that `matrix.rank` is equal to the row-rank, and that `rank Aᵀ = rank A`.
 
 -/
 
@@ -34,62 +34,79 @@ namespace Matrix
 
 open FiniteDimensional
 
-variable {m n o R : Type _} [m_fin : Fintype m] [Fintype n] [Fintype o]
+variable {l m n o R : Type _} [m_fin : Fintype m] [Fintype n] [Fintype o]
 
-variable [DecidableEq n] [DecidableEq o] [CommRing R]
+variable [CommRing R]
 
 /-- The rank of a matrix is the rank of its image. -/
 noncomputable def rank (A : Matrix m n R) : ℕ :=
-  finrank R A.toLin'.range
+  finrank R A.mulVecLin.range
 #align matrix.rank Matrix.rank
 
 @[simp]
-theorem rank_one [StrongRankCondition R] : rank (1 : Matrix n n R) = Fintype.card n := by
-  rw [rank, to_lin'_one, LinearMap.range_id, finrank_top, finrank_pi]
+theorem rank_one [StrongRankCondition R] [DecidableEq n] :
+    rank (1 : Matrix n n R) = Fintype.card n := by
+  rw [rank, mul_vec_lin_one, LinearMap.range_id, finrank_top, finrank_pi]
 #align matrix.rank_one Matrix.rank_one
 
 @[simp]
 theorem rank_zero [Nontrivial R] : rank (0 : Matrix m n R) = 0 := by
-  rw [rank, LinearEquiv.map_zero, LinearMap.range_zero, finrank_bot]
+  rw [rank, mul_vec_lin_zero, LinearMap.range_zero, finrank_bot]
 #align matrix.rank_zero Matrix.rank_zero
 
 theorem rank_le_card_width [StrongRankCondition R] (A : Matrix m n R) : A.rank ≤ Fintype.card n :=
   by
   haveI : Module.Finite R (n → R) := Module.Finite.pi
   haveI : Module.Free R (n → R) := Module.Free.pi _ _
-  exact A.to_lin'.finrank_range_le.trans_eq (finrank_pi _)
+  exact A.mul_vec_lin.finrank_range_le.trans_eq (finrank_pi _)
 #align matrix.rank_le_card_width Matrix.rank_le_card_width
 
 theorem rank_le_width [StrongRankCondition R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) :
     A.rank ≤ n :=
   A.rank_le_card_width.trans <| (Fintype.card_fin n).le
 #align matrix.rank_le_width Matrix.rank_le_width
 
-theorem rank_mul_le [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) :
+theorem rank_mul_le_left [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) :
     (A ⬝ B).rank ≤ A.rank := by
-  rw [rank, rank, to_lin'_mul]
+  rw [rank, rank, mul_vec_lin_mul]
   exact Cardinal.toNat_le_of_le_of_lt_aleph0 (rank_lt_aleph_0 _ _) (LinearMap.rank_comp_le_left _ _)
+#align matrix.rank_mul_le_left Matrix.rank_mul_le_left
+
+include m_fin
+
+theorem rank_mul_le_right [StrongRankCondition R] (A : Matrix l m R) (B : Matrix m n R) :
+    (A ⬝ B).rank ≤ B.rank := by
+  rw [rank, rank, mul_vec_lin_mul]
+  exact
+    finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _) (rank_lt_aleph_0 _ _)
+#align matrix.rank_mul_le_right Matrix.rank_mul_le_right
+
+omit m_fin
+
+theorem rank_mul_le [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) :
+    (A ⬝ B).rank ≤ min A.rank B.rank :=
+  le_min (rank_mul_le_left _ _) (rank_mul_le_right _ _)
 #align matrix.rank_mul_le Matrix.rank_mul_le
 
-theorem rank_unit [StrongRankCondition R] (A : (Matrix n n R)ˣ) :
+theorem rank_unit [StrongRankCondition R] [DecidableEq n] (A : (Matrix n n R)ˣ) :
     (A : Matrix n n R).rank = Fintype.card n :=
   by
   refine' le_antisymm (rank_le_card_width A) _
-  have := rank_mul_le (A : Matrix n n R) (↑A⁻¹ : Matrix n n R)
+  have := rank_mul_le_left (A : Matrix n n R) (↑A⁻¹ : Matrix n n R)
   rwa [← mul_eq_mul, ← Units.val_mul, mul_inv_self, Units.val_one, rank_one] at this
 #align matrix.rank_unit Matrix.rank_unit
 
-theorem rank_of_isUnit [StrongRankCondition R] (A : Matrix n n R) (h : IsUnit A) :
+theorem rank_of_isUnit [StrongRankCondition R] [DecidableEq n] (A : Matrix n n R) (h : IsUnit A) :
     A.rank = Fintype.card n := by
   obtain ⟨A, rfl⟩ := h
   exact rank_unit A
 #align matrix.rank_of_is_unit Matrix.rank_of_isUnit
 
 include m_fin
 
-theorem rank_eq_finrank_range_toLin {M₁ M₂ : Type _} [AddCommGroup M₁] [AddCommGroup M₂]
-    [Module R M₁] [Module R M₂] (A : Matrix m n R) (v₁ : Basis m R M₁) (v₂ : Basis n R M₂) :
-    A.rank = finrank R (toLin v₂ v₁ A).range :=
+theorem rank_eq_finrank_range_toLin [DecidableEq n] {M₁ M₂ : Type _} [AddCommGroup M₁]
+    [AddCommGroup M₂] [Module R M₁] [Module R M₂] (A : Matrix m n R) (v₁ : Basis m R M₁)
+    (v₂ : Basis n R M₂) : A.rank = finrank R (toLin v₂ v₁ A).range :=
   by
   let e₁ := (Pi.basisFun R m).Equiv v₁ (Equiv.refl _)
   let e₂ := (Pi.basisFun R n).Equiv v₂ (Equiv.refl _)
@@ -105,7 +122,7 @@ theorem rank_eq_finrank_range_toLin {M₁ M₂ : Type _} [AddCommGroup M₁] [Ad
   apply LinearMap.ext_ring
   have aux₁ := to_lin_self (Pi.basisFun R n) (Pi.basisFun R m) A i
   have aux₂ := Basis.equiv_apply (Pi.basisFun R n) i v₂
-  rw [to_lin_eq_to_lin'] at aux₁
+  rw [to_lin_eq_to_lin', to_lin'_apply'] at aux₁
   rw [Pi.basisFun_apply, LinearMap.coe_stdBasis] at aux₁ aux₂
   simp only [LinearMap.comp_apply, e₁, e₂, LinearEquiv.coe_coe, Equiv.refl_apply, aux₁, aux₂,
     LinearMap.coe_single, to_lin_self, LinearEquiv.map_sum, LinearEquiv.map_smul, Basis.equiv_apply]
@@ -125,5 +142,10 @@ theorem rank_le_height [StrongRankCondition R] {m n : ℕ} (A : Matrix (Fin m) (
   A.rank_le_card_height.trans <| (Fintype.card_fin m).le
 #align matrix.rank_le_height Matrix.rank_le_height
 
+/-- The rank of a matrix is the rank of the space spanned by its columns. -/
+theorem rank_eq_finrank_span_cols (A : Matrix m n R) :
+    A.rank = finrank R (Submodule.span R (Set.range Aᵀ)) := by rw [rank, Matrix.range_mulVecLin]
+#align matrix.rank_eq_finrank_span_cols Matrix.rank_eq_finrank_span_cols
+
 end Matrix
 

Mathbin/GroupTheory/SpecificGroups/Alternating.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 
 ! This file was ported from Lean 3 source module group_theory.specific_groups.alternating
-! leanprover-community/mathlib commit 0f6670b8af2dff699de1c0b4b49039b31bc13c46
+! leanprover-community/mathlib commit 9a48a083b390d9b84a71efbdc4e8dfa26a687104
 ! 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.IntervalCases
 /-!
 # Alternating Groups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The alternating group on a finite type `α` is the subgroup of the permutation group `perm α`
 consisting of the even permutations.
 

Mathbin/LinearAlgebra/Dimension.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl, Sander Dahmen, Scott Morrison
 
 ! This file was ported from Lean 3 source module linear_algebra.dimension
-! leanprover-community/mathlib commit b5b5dd5a47b5744260e2c9185013075ce9dadccd
+! leanprover-community/mathlib commit 47a5f8186becdbc826190ced4312f8199f9db6a5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1876,14 +1876,34 @@ theorem rank_comp_le_left (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.
 #align linear_map.rank_comp_le_left LinearMap.rank_comp_le_left
 -/
 
+theorem lift_rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
+    Cardinal.lift.{v'} (rank (f.comp g)) ≤ Cardinal.lift.{v''} (rank g) := by
+  rw [rank, rank, LinearMap.range_comp] <;> exact lift_rank_map_le _ _
+#align linear_map.lift_rank_comp_le_right LinearMap.lift_rank_comp_le_right
+
+/-- The rank of the composition of two maps is less than the minimum of their ranks. -/
+theorem lift_rank_comp_le (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
+    Cardinal.lift.{v'} (rank (f.comp g)) ≤
+      min (Cardinal.lift.{v'} (rank f)) (Cardinal.lift.{v''} (rank g)) :=
+  le_min (Cardinal.lift_le.mpr <| rank_comp_le_left _ _) (lift_rank_comp_le_right _ _)
+#align linear_map.lift_rank_comp_le LinearMap.lift_rank_comp_le
+
 variable [AddCommGroup V'₁] [Module K V'₁]
 
 #print LinearMap.rank_comp_le_right /-
 theorem rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ rank g := by
-  rw [rank, rank, LinearMap.range_comp] <;> exact rank_map_le _ _
+  simpa only [Cardinal.lift_id] using lift_rank_comp_le_right g f
 #align linear_map.rank_comp_le_right LinearMap.rank_comp_le_right
 -/
 
+/-- The rank of the composition of two maps is less than the minimum of their ranks.
+
+See `lift_rank_comp_le` for the universe-polymorphic version. -/
+theorem rank_comp_le (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) :
+    rank (f.comp g) ≤ min (rank f) (rank g) := by
+  simpa only [Cardinal.lift_id] using lift_rank_comp_le g f
+#align linear_map.rank_comp_le LinearMap.rank_comp_le
+
 end Ring
 
 section DivisionRing