Skip to content

Commit 54843da

Browse files
YaelDilliesYaelDillies
committed
chore: Move order theory and algebra out of Data.Fin.Tuple.Basic 
1 parent 4bf28bb commit 54843da

35 files changed

+400
-399
lines changed

‎Archive/Imo/Imo1994Q1.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Antoine Labelle. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Antoine Labelle
55
-/
6-
import Mathlib.Algebra.Group.Fin
6+
import Mathlib.Algebra.Group.Fin.Basic
77
import Mathlib.Algebra.Order.BigOperators.Group.Finset
88
import Mathlib.Data.Finset.Sort
99
import Mathlib.Order.Interval.Finset.Fin

‎Mathlib.lean

+4-3
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,8 @@ import Mathlib.Algebra.Group.Equiv.Basic
214214
import Mathlib.Algebra.Group.Equiv.TypeTags
215215
import Mathlib.Algebra.Group.Even
216216
import Mathlib.Algebra.Group.Ext
217-
import Mathlib.Algebra.Group.Fin
217+
import Mathlib.Algebra.Group.Fin.Basic
218+
import Mathlib.Algebra.Group.Fin.Tuple
218219
import Mathlib.Algebra.Group.FiniteSupport
219220
import Mathlib.Algebra.Group.Hom.Basic
220221
import Mathlib.Algebra.Group.Hom.CompTypeclasses
@@ -1903,7 +1904,6 @@ import Mathlib.Data.Fin.Tuple.Basic
19031904
import Mathlib.Data.Fin.Tuple.BubbleSortInduction
19041905
import Mathlib.Data.Fin.Tuple.Curry
19051906
import Mathlib.Data.Fin.Tuple.Finset
1906-
import Mathlib.Data.Fin.Tuple.Monotone
19071907
import Mathlib.Data.Fin.Tuple.NatAntidiagonal
19081908
import Mathlib.Data.Fin.Tuple.Reflection
19091909
import Mathlib.Data.Fin.Tuple.Sort
@@ -3324,7 +3324,8 @@ import Mathlib.Order.Filter.SmallSets
33243324
import Mathlib.Order.Filter.Subsingleton
33253325
import Mathlib.Order.Filter.Ultrafilter
33263326
import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
3327-
import Mathlib.Order.Fin
3327+
import Mathlib.Order.Fin.Basic
3328+
import Mathlib.Order.Fin.Tuple
33283329
import Mathlib.Order.FixedPoints
33293330
import Mathlib.Order.GaloisConnection
33303331
import Mathlib.Order.GameAdd

‎Mathlib/Algebra/CharP/Defs.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau, Joey van Langen, Casper Putz
55
-/
6-
import Mathlib.Algebra.Group.Fin
6+
import Mathlib.Algebra.Group.Fin.Basic
77
import Mathlib.Algebra.Group.ULift
88
import Mathlib.Data.Int.ModEq
99
import Mathlib.Data.Nat.Cast.Prod

‎Mathlib/Algebra/Group/Fin.lean ‎Mathlib/Algebra/Group/Fin/Basic.lean

File renamed without changes.

‎Mathlib/Algebra/Group/Fin/Tuple.lean

+164
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
/-
2+
Copyright (c) 2019 Floris van Doorn. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Floris van Doorn, Yury Kudryashov, Sébastien Gouëzel, Chris Hughes
5+
-/
6+
import Mathlib.Algebra.Group.Basic
7+
import Mathlib.Algebra.Group.Pi.Basic
8+
import Mathlib.Data.Fin.VecNotation
9+
10+
#align_import data.fin.tuple.basic from "leanprover-community/mathlib"@"ef997baa41b5c428be3fb50089a7139bf4ee886b"
11+
12+
/-!
13+
# Algebraic properties of tuples
14+
-/
15+
16+
namespace Fin
17+
variable {m n : ℕ} {α : Fin (n + 1) → Type*}
18+
19+
@[to_additive (attr := simp)]
20+
lemma insertNth_one_right [∀ j, One (α j)] (i : Fin (n + 1)) (x : α i) :
21+
i.insertNth x 1 = Pi.mulSingle i x :=
22+
insertNth_eq_iff.2 <| by simp [succAbove_ne, Pi.one_def]
23+
#align fin.insert_nth_zero_right Fin.insertNth_zero_right
24+
25+
@[to_additive (attr := simp)]
26+
lemma insertNth_mul [∀ j, Mul (α j)] (i : Fin (n + 1)) (x y : α i) (p q : ∀ j, α (i.succAbove j)) :
27+
i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q :=
28+
insertNth_binop (fun _ ↦ (· * ·)) i x y p q
29+
#align fin.insert_nth_mul Fin.insertNth_mul
30+
#align fin.insert_nth_add Fin.insertNth_add
31+
32+
@[to_additive (attr := simp)]
33+
lemma insertNth_div [∀ j, Div (α j)] (i : Fin (n + 1)) (x y : α i)(p q : ∀ j, α (i.succAbove j)) :
34+
i.insertNth (x / y) (p / q) = i.insertNth x p / i.insertNth y q :=
35+
insertNth_binop (fun _ ↦ (· / ·)) i x y p q
36+
#align fin.insert_nth_div Fin.insertNth_div
37+
#align fin.insert_nth_sub Fin.insertNth_sub
38+
39+
@[to_additive (attr := simp)]
40+
lemma insertNth_div_same [∀ j, Group (α j)] (i : Fin (n + 1)) (x y : α i)
41+
(p : ∀ j, α (i.succAbove j)) : i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y) := by
42+
simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]
43+
#align fin.insert_nth_sub_same Fin.insertNth_sub_same
44+
45+
end Fin
46+
47+
namespace Matrix
48+
49+
variable {α M : Type*} {n : ℕ}
50+
51+
section SMul
52+
variable [SMul M α]
53+
54+
@[simp] lemma smul_empty (x : M) (v : Fin 0 → α) : x • v = ![] := empty_eq _
55+
#align matrix.smul_empty Matrix.smul_empty
56+
57+
@[simp] lemma smul_cons (x : M) (y : α) (v : Fin n → α) :
58+
x • vecCons y v = vecCons (x • y) (x • v) := by ext i; refine i.cases ?_ ?_ <;> simp
59+
#align matrix.smul_cons Matrix.smul_cons
60+
61+
end SMul
62+
63+
section Add
64+
variable [Add α]
65+
66+
@[simp] lemma empty_add_empty (v w : Fin 0 → α) : v + w = ![] := empty_eq _
67+
#align matrix.empty_add_empty Matrix.empty_add_empty
68+
69+
@[simp] lemma cons_add (x : α) (v : Fin n → α) (w : Fin n.succ → α) :
70+
vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w) := by
71+
ext i; refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]
72+
#align matrix.cons_add Matrix.cons_add
73+
74+
@[simp] lemma add_cons (v : Fin n.succ → α) (y : α) (w : Fin n → α) :
75+
v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w) := by
76+
ext i; refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]
77+
#align matrix.add_cons Matrix.add_cons
78+
79+
lemma cons_add_cons (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) :
80+
vecCons x v + vecCons y w = vecCons (x + y) (v + w) := by simp
81+
#align matrix.cons_add_cons Matrix.cons_add_cons
82+
83+
@[simp] lemma head_add (a b : Fin n.succ → α) : vecHead (a + b) = vecHead a + vecHead b := rfl
84+
#align matrix.head_add Matrix.head_add
85+
86+
@[simp] lemma tail_add (a b : Fin n.succ → α) : vecTail (a + b) = vecTail a + vecTail b := rfl
87+
#align matrix.tail_add Matrix.tail_add
88+
89+
end Add
90+
91+
section Sub
92+
variable [Sub α]
93+
94+
@[simp] lemma empty_sub_empty (v w : Fin 0 → α) : v - w = ![] := empty_eq _
95+
#align matrix.empty_sub_empty Matrix.empty_sub_empty
96+
97+
@[simp] lemma cons_sub (x : α) (v : Fin n → α) (w : Fin n.succ → α) :
98+
vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w) := by
99+
ext i; refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]
100+
#align matrix.cons_sub Matrix.cons_sub
101+
102+
@[simp] lemma sub_cons (v : Fin n.succ → α) (y : α) (w : Fin n → α) :
103+
v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w) := by
104+
ext i; refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]
105+
#align matrix.sub_cons Matrix.sub_cons
106+
107+
lemma cons_sub_cons (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) :
108+
vecCons x v - vecCons y w = vecCons (x - y) (v - w) := by simp
109+
#align matrix.cons_sub_cons Matrix.cons_sub_cons
110+
111+
@[simp] lemma head_sub (a b : Fin n.succ → α) : vecHead (a - b) = vecHead a - vecHead b := rfl
112+
#align matrix.head_sub Matrix.head_sub
113+
114+
@[simp] lemma tail_sub (a b : Fin n.succ → α) : vecTail (a - b) = vecTail a - vecTail b := rfl
115+
#align matrix.tail_sub Matrix.tail_sub
116+
117+
end Sub
118+
119+
section Zero
120+
variable [Zero α]
121+
122+
@[simp] lemma zero_empty : (0 : Fin 0 → α) = ![] := empty_eq _
123+
#align matrix.zero_empty Matrix.zero_empty
124+
125+
@[simp] lemma cons_zero_zero : vecCons (0 : α) (0 : Fin n → α) = 0 := by
126+
ext i; exact i.cases rfl (by simp)
127+
#align matrix.cons_zero_zero Matrix.cons_zero_zero
128+
129+
@[simp] lemma head_zero : vecHead (0 : Fin n.succ → α) = 0 := rfl
130+
#align matrix.head_zero Matrix.head_zero
131+
132+
@[simp] lemma tail_zero : vecTail (0 : Fin n.succ → α) = 0 := rfl
133+
#align matrix.tail_zero Matrix.tail_zero
134+
135+
@[simp] lemma cons_eq_zero_iff {v : Fin n → α} {x : α} : vecCons x v = 0 ↔ x = 0 ∧ v = 0 where
136+
mp h := ⟨congr_fun h 0, by convert congr_arg vecTail h⟩
137+
mpr := fun ⟨hx, hv⟩ ↦ by simp [hx, hv]
138+
#align matrix.cons_eq_zero_iff Matrix.cons_eq_zero_iff
139+
140+
lemma cons_nonzero_iff {v : Fin n → α} {x : α} : vecCons x v ≠ 0 ↔ x ≠ 0 ∨ v ≠ 0 where
141+
mp h := not_and_or.mp (h ∘ cons_eq_zero_iff.mpr)
142+
mpr h := mt cons_eq_zero_iff.mp (not_and_or.mpr h)
143+
#align matrix.cons_nonzero_iff Matrix.cons_nonzero_iff
144+
145+
end Zero
146+
147+
section Neg
148+
variable [Neg α]
149+
150+
@[simp] lemma neg_empty (v : Fin 0 → α) : -v = ![] := empty_eq _
151+
#align matrix.neg_empty Matrix.neg_empty
152+
153+
@[simp] lemma neg_cons (x : α) (v : Fin n → α) : -vecCons x v = vecCons (-x) (-v) := by
154+
ext i; refine i.cases ?_ ?_ <;> simp
155+
#align matrix.neg_cons Matrix.neg_cons
156+
157+
@[simp] lemma head_neg (a : Fin n.succ → α) : vecHead (-a) = -vecHead a := rfl
158+
#align matrix.head_neg Matrix.head_neg
159+
160+
@[simp] lemma tail_neg (a : Fin n.succ → α) : vecTail (-a) = -vecTail a := rfl
161+
#align matrix.tail_neg Matrix.tail_neg
162+
163+
end Neg
164+
end Matrix

‎Mathlib/Algebra/Order/Antidiag/Finsupp.lean

+1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Eric Wieser, Bhavik Mehta
55
-/
66
import Mathlib.Algebra.Order.Antidiag.Pi
7+
import Mathlib.Data.Finsupp.Defs
78
import Mathlib.Data.Finsupp.Basic
89

910
/-!

‎Mathlib/Algebra/Order/Antidiag/Pi.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ where
4545
match d with
4646
| 0 =>
4747
if h : n = 0 then
48-
⟨{0}, by simp [h, Subsingleton.elim finZeroElim ![]]⟩
48+
⟨{0}, by simp [h, Subsingleton.elim _ ![]]⟩
4949
else
5050
⟨∅, by simp [Ne.symm h]⟩
5151
| d + 1 =>

‎Mathlib/Analysis/BoxIntegral/Box/Basic.lean

+1
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov
55
-/
6+
import Mathlib.Order.Fin.Tuple
67
import Mathlib.Order.Interval.Set.Monotone
78
import Mathlib.Topology.MetricSpace.Basic
89
import Mathlib.Topology.MetricSpace.Bounded

‎Mathlib/CategoryTheory/ComposableArrows.lean

+1
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Joël Riou
66
import Mathlib.CategoryTheory.Category.Preorder
77
import Mathlib.CategoryTheory.EqToHom
88
import Mathlib.CategoryTheory.Functor.Const
9+
import Mathlib.Order.Fin.Basic
910
import Mathlib.Tactic.FinCases
1011

1112
/-!

‎Mathlib/Control/Random.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Henrik Böving
55
-/
66
import Mathlib.Control.ULiftable
7-
import Mathlib.Order.Fin
7+
import Mathlib.Order.Fin.Basic
88

99
#align_import control.random from "leanprover-community/mathlib"@"fdc286cc6967a012f41b87f76dcd2797b53152af"
1010

‎Mathlib/Data/Array/Lemmas.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Leonardo de Moura, Mario Carneiro
55
-/
6-
import Mathlib.Algebra.Group.Fin
6+
import Mathlib.Algebra.Group.Fin.Basic
77
import Mathlib.Data.List.Basic
88

99
#align_import data.array.lemmas from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"

‎Mathlib/Data/Fin/FlagRange.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Yury Kudryashov
66
import Mathlib.Data.Fin.Basic
77
import Mathlib.Order.Chain
88
import Mathlib.Order.Cover
9-
import Mathlib.Order.Fin
9+
import Mathlib.Order.Fin.Basic
1010

1111
/-!
1212
# Range of `f : Fin (n + 1) → α` as a `Flag`

‎Mathlib/Data/Fin/SuccPred.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Copyright (c) 2022 Eric Rodriguez. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Eric Rodriguez
55
-/
6-
import Mathlib.Algebra.Group.Fin
7-
import Mathlib.Order.Fin
6+
import Mathlib.Algebra.Group.Fin.Basic
7+
import Mathlib.Order.Fin.Basic
88
import Mathlib.Order.SuccPred.Basic
99

1010
#align_import data.fin.succ_pred from "leanprover-community/mathlib"@"7c523cb78f4153682c2929e3006c863bfef463d0"

0 commit comments

Comments
 (0)