Skip to content

Commit

Permalink
bump to nightly-2023-06-13-21
Browse files Browse the repository at this point in the history 
mathlib commit leanprover-community/mathlib@9fb8964
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed Jun 13, 2023
1 parent f0af529 commit 829520a
Show file tree
Hide file tree
Showing 2,670 changed files with 131,813 additions and 4,228 deletions.
3 changes: 0 additions & 3 deletions Archive/100-theorems-list/57HeronsFormula.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,14 +30,11 @@ open scoped Real EuclideanGeometry

namespace Theorems100

-- mathport name: «expr√»
local notation "√" => Real.sqrt

variable {V : Type _} {P : Type _} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
[NormedAddTorsor V P]

include V

/-- **Heron's formula**: The area of a triangle with side lengths `a`, `b`, and `c` is
`√(s * (s - a) * (s - b) * (s - c))` where `s = (a + b + c) / 2` is the semiperimeter.
We show this by equating this formula to `a * b * sin γ`, where `γ` is the angle opposite
Expand Down
8 changes: 0 additions & 8 deletions Archive/100-theorems-list/82CubingACube.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,8 +164,6 @@ namespace Correct

variable (h : Correct cs)

include h

theorem toSet_subset_unitCube {i} : (cs i).to_set ⊆ unitCube.to_set :=
h.iUnion_eq ▸ subset_iUnion _ i
#align theorems_100.«82».correct.to_set_subset_unit_cube Theorems100.«82».Correct.toSet_subset_unitCube
Expand Down Expand Up @@ -301,8 +299,6 @@ theorem t_le_t (hi : i ∈ bcubes cs c) (j : Fin n) : (cs i).b j.succ + (cs i).w
exact h'.2; simp [hw]
#align theorems_100.«82».t_le_t Theorems100.«82».t_le_t

include h v

/-- Every cube in the valley must be smaller than it -/
theorem w_lt_w (hi : i ∈ bcubes cs c) : (cs i).w < c.w :=
by
Expand Down Expand Up @@ -558,8 +554,6 @@ theorem valley_mi : Valley cs (cs (mi h v)).shiftUp :=

variable (h) [Nontrivial ι]

omit v

/-- We get a sequence of cubes whose size is decreasing -/
noncomputable def sequenceOfCubes : ℕ → { i : ι // Valley cs (cs i).shiftUp }
| 0 =>
Expand All @@ -586,8 +580,6 @@ theorem injective_sequenceOfCubes : Injective (sequenceOfCubes h) :=
(strictAnti_sequence_of_cubes h).Injective
#align theorems_100.«82».injective_sequence_of_cubes Theorems100.«82».injective_sequenceOfCubes

omit h

/-- The infinite sequence of cubes contradicts the finiteness of the family. -/
theorem not_correct : ¬Correct cs := fun h =>
(Finite.of_injective _ <| injective_sequenceOfCubes h).False
Expand Down
6 changes: 0 additions & 6 deletions Archive/100-theorems-list/83FriendshipGraphs.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,6 @@ end FriendshipDef

variable [Fintype V] {G : SimpleGraph V} {d : ℕ} (hG : Friendship G)

include hG

namespace Friendship

variable (R)
Expand Down Expand Up @@ -214,8 +212,6 @@ theorem card_mod_p_of_regular {p : ℕ} (dmod : (d : ZMod p) = 1) (hd : G.IsRegu

end Nonempty

omit hG

theorem adjMatrix_sq_mul_const_one_of_regular (hd : G.IsRegularOfDegree d) :
(G.adjMatrix R * fun _ _ => 1) = fun _ _ => d := by ext x; simp [← hd x, degree]
#align theorems_100.friendship.adj_matrix_sq_mul_const_one_of_regular Theorems100.Friendship.adjMatrix_sq_mul_const_one_of_regular
Expand All @@ -225,8 +221,6 @@ theorem adjMatrix_mul_const_one_mod_p_of_regular {p : ℕ} (dmod : (d : ZMod p)
rw [adj_matrix_sq_mul_const_one_of_regular hd, dmod]
#align theorems_100.friendship.adj_matrix_mul_const_one_mod_p_of_regular Theorems100.Friendship.adjMatrix_mul_const_one_mod_p_of_regular

include hG

/-- Modulo a factor of `d-1`, the square and all higher powers of the adjacency matrix
of a `d`-regular friendship graph reduce to the matrix whose entries are all 1. -/
theorem adjMatrix_pow_mod_p_of_regular {p : ℕ} (dmod : (d : ZMod p) = 1)
Expand Down
2 changes: 0 additions & 2 deletions Archive/100-theorems-list/93BirthdayProblem.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,10 +25,8 @@ uses is `fintype.card_embedding_eq`.

namespace Theorems100

-- mathport name: finset.card
local notation "|" x "|" => Finset.card x

-- mathport name: fintype.card
local notation "‖" x "‖" => Fintype.card x

/-- **Birthday Problem**: set cardinality interpretation. -/
Expand Down
2 changes: 0 additions & 2 deletions Archive/Arithcc.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -208,7 +208,6 @@ def StateEqRs (t : Register) (ζ₁ ζ₂ : State) : Prop :=
∀ r : Register, r < t → ζ₁.rs r = ζ₂.rs r
#align arithcc.state_eq_rs Arithcc.StateEqRs

-- mathport name: «expr ≃[ ]/ac »
notation:50 ζ₁ " ≃[" t "]/ac " ζ₂:50 => StateEqRs t ζ₁ ζ₂

@[refl]
Expand All @@ -230,7 +229,6 @@ def StateEq (t : Register) (ζ₁ ζ₂ : State) : Prop :=
ζ₁.ac = ζ₂.ac ∧ StateEqRs t ζ₁ ζ₂
#align arithcc.state_eq Arithcc.StateEq

-- mathport name: «expr ≃[ ] »
notation:50 ζ₁ " ≃[" t "] " ζ₂:50 => StateEq t ζ₁ ζ₂

@[refl]
Expand Down
4 changes: 0 additions & 4 deletions Archive/Examples/PropEncodable.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,16 +76,12 @@ namespace PropForm
private def constructors (α : Type _) :=
Sum α (Sum Unit (Sum Unit Unit))

-- mathport name: «exprcvar »
local notation "cvar " a => Sum.inl a

-- mathport name: exprcnot
local notation "cnot" => Sum.inr (Sum.inl Unit.unit)

-- mathport name: exprcand
local notation "cand" => Sum.inr (Sum.inr (Sum.inr Unit.unit))

-- mathport name: exprcor
local notation "cor" => Sum.inr (Sum.inr (Sum.inl Unit.unit))

@[simp]
Expand Down
2 changes: 0 additions & 2 deletions Archive/Imo/Imo1975Q1.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,6 @@ variable (hx : AntitoneOn x (Finset.Icc 1 n))

variable (hy : AntitoneOn y (Finset.Icc 1 n))

include hx hy hσ

theorem imo1975_q1 :
∑ i in Finset.Icc 1 n, (x i - y i) ^ 2 ≤ ∑ i in Finset.Icc 1 n, (x i - y (σ i)) ^ 2 :=
by
Expand Down
4 changes: 0 additions & 4 deletions Archive/Imo/Imo1981Q3.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -158,8 +158,6 @@ satisfying `nat_predicate m n N` are `fib K` and `fib (K+1)`, respectively.
-/
variable {K : ℕ} (HK : N < fib K + fib (K + 1)) {N}

include HK

theorem m_n_bounds {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ fib K ∧ n ≤ fib (K + 1) :=
by
obtain ⟨k : ℕ, hm : m = fib k, hn : n = fib (k + 1)⟩ := h1.imp_fib m
Expand Down Expand Up @@ -190,8 +188,6 @@ We spell out the consequences of this result for `specified_set N` here.
-/
variable {M : ℕ} (HM : M = fib K ^ 2 + fib (K + 1) ^ 2)

include HM

theorem k_bound {m n : ℤ} (h1 : ProblemPredicate N m n) : m ^ 2 + n ^ 2 ≤ M :=
by
have h2 : 0 ≤ m := h1.m_range.left.le
Expand Down
2 changes: 0 additions & 2 deletions Archive/Imo/Imo2019Q2.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,8 +74,6 @@ variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]

variable [NormedAddTorsor V Pt] [hd2 : Fact (finrank ℝ V = 2)]

include hd2

namespace imo2019_q2

noncomputable section
Expand Down
5 changes: 0 additions & 5 deletions Archive/Sensitivity.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,6 @@ open scoped Classical

open scoped BigOperators

-- mathport name: «expr√»
notation "√" => Real.sqrt

open Function Bool LinearMap Fintype FiniteDimensional Module.DualBases
Expand Down Expand Up @@ -380,26 +379,22 @@ In this section, in order to enforce that `n` is positive, we write it as
/-! `dim X` will denote the dimension of a subspace `X` as a cardinal. -/


-- mathport name: «exprdim »
notation "dim " X:70 => Module.rank ℝ ↥X

/-! `fdim X` will denote the (finite) dimension of a subspace `X` as a natural number. -/


-- mathport name: exprfdim
notation "fdim" => finrank ℝ

/-! `Span S` will denote the ℝ-subspace spanned by `S`. -/


-- mathport name: exprSpan
notation "Span" => Submodule.span ℝ

/-! `Card X` will denote the cardinal of a subset of a finite type, as a
natural number. -/


-- mathport name: «exprCard »
notation "Card " X:70 => X.toFinset.card

/-! In the following, `⊓` and `⊔` will denote intersection and sums of ℝ-subspaces,
Expand Down
2 changes: 0 additions & 2 deletions Counterexamples/DirectSumIsInternal.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,10 +41,8 @@ def withSign (i : ℤˣ) : Submodule ℕ ℤ :=
exact add_nonneg hx hy }
#align counterexample.with_sign Counterexample.withSign

-- mathport name: «exprℤ≥0»
local notation "ℤ≥0" => withSign 1

-- mathport name: «exprℤ≤0»
local notation "ℤ≤0" => withSign (-1)

theorem mem_withSign_one {x : ℤ} : x ∈ ℤ≥0 ↔ 0 ≤ x :=
Expand Down
1 change: 0 additions & 1 deletion Counterexamples/HomogeneousPrimeNotPrime.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,6 @@ theorem grading.mul_mem :

end

-- mathport name: exprR
local notation "R" => ZMod 4

/-- `R² ≅ {(a, a) | a ∈ R} ⨁ {(0, b) | b ∈ R}` by `(x, y) ↦ (x, x) + (0, y - x)`. -/
Expand Down
1 change: 0 additions & 1 deletion Counterexamples/LinearOrderWithPosMulPosEqZero.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,6 @@ instance : Zero Foo :=
instance : One Foo :=
⟨one⟩

-- mathport name: exprε
local notation "ε" => eps

/-- The order on `foo` is the one induced by the natural order on the image of `aux1`. -/
Expand Down
2 changes: 0 additions & 2 deletions Counterexamples/MapFloor.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,10 +53,8 @@ def IntWithEpsilon :=
deriving CommRing, Nontrivial, Inhabited
#align counterexample.int_with_epsilon Counterexample.IntWithEpsilon

-- mathport name: «exprℤ[ε]»
local notation "ℤ[ε]" => IntWithEpsilon

-- mathport name: exprε
local notation "ε" => (X : ℤ[ε])

namespace IntWithEpsilon
Expand Down
1 change: 0 additions & 1 deletion Counterexamples/SorgenfreyLine.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,6 @@ def SorgenfreyLine : Type :=
deriving ConditionallyCompleteLinearOrder, LinearOrderedField, Archimedean
#align counterexample.sorgenfrey_line Counterexample.SorgenfreyLine

-- mathport name: sorgenfrey_line
scoped[SorgenfreyLine] notation "ℝₗ" => SorgenfreyLine

namespace SorgenfreyLine
Expand Down
2 changes: 0 additions & 2 deletions Mathbin/Algebra/Abs.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,9 +65,7 @@ class NegPart (α : Type _) where
#align has_neg_part NegPart
-/

-- mathport name: «expr ⁺»
postfix:1000 "⁺" => PosPart.pos

-- mathport name: «expr ⁻»
postfix:1000 "⁻" => NegPart.neg

Loading

0 comments on commit 829520a

Please sign in to comment.