ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>InvolutiveNeg ι<VAR>s : Finset ι<VAR>f : ι → α<GOAL>∑ i ∈ -s, f i = ∑ i ∈ s, f (-i)
<VAR>α : Type u_2<VAR>CommMonoid α<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>InvolutiveInv ι<VAR>s : Finset ι<VAR>f : ι → α<GOAL>∏ i ∈ s⁻¹, f i = ∏ i ∈ s, f i⁻¹
<VAR>α : Type u_2<VAR>CommMonoid α<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>InvolutiveNeg ι<VAR>s : Finset ι<VAR>f : ι → α<GOAL>∏ i ∈ -s, f i = ∏ i ∈ s, f (-i)
<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>InvolutiveInv ι<VAR>s : Finset ι<VAR>f : ι → α<GOAL>∑ i ∈ s⁻¹, f i = ∑ i ∈ s, f i⁻¹
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → Mul (α i)<VAR>s t : (i : ι) → Finset (α i)<GOAL>(Fintype.piFinset fun i => s i * t i) = Fintype.piFinset s * Fintype.piFinset t
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → Add (α i)<VAR>s t : (i : ι) → Finset (α i)<GOAL>(Fintype.piFinset fun i => s i + t i) = Fintype.piFinset s + Fintype.piFinset t
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → Sub (α i)<VAR>s t : (i : ι) → Finset (α i)<GOAL>(Fintype.piFinset fun i => s i - t i) = Fintype.piFinset s - Fintype.piFinset t
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → Div (α i)<VAR>s t : (i : ι) → Finset (α i)<GOAL>(Fintype.piFinset fun i => s i / t i) = Fintype.piFinset s / Fintype.piFinset t
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → Neg (α i)<VAR>s : (i : ι) → Finset (α i)<GOAL>(Fintype.piFinset fun i => -s i) = -Fintype.piFinset s
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → Inv (α i)<VAR>s : (i : ι) → Finset (α i)<GOAL>(Fintype.piFinset fun i => (s i)⁻¹) = (Fintype.piFinset s)⁻¹
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>β : ι → Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → VAdd (α i) (β i)<VAR>s : (i : ι) → Finset (α i)<VAR>t : (i : ι) → Finset (β i)<GOAL>(Fintype.piFinset fun i => s i +ᵥ t i) = Fintype.piFinset s +ᵥ Fintype.piFinset t
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>β : ι → Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → SMul (α i) (β i)<VAR>s : (i : ι) → Finset (α i)<VAR>t : (i : ι) → Finset (β i)<GOAL>(Fintype.piFinset fun i => s i • t i) = Fintype.piFinset s • Fintype.piFinset t
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>β : ι → Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → VAdd (α i) (β i)<VAR>a : (i : ι) → α i<VAR>s : (i : ι) → Finset (β i)<GOAL>(Fintype.piFinset fun i => a i +ᵥ s i) = a +ᵥ Fintype.piFinset s
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>β : ι → Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → SMul (α i) (β i)<VAR>a : (i : ι) → α i<VAR>s : (i : ι) → Finset (β i)<GOAL>(Fintype.piFinset fun i => a i • s i) = a • Fintype.piFinset s
<VAR>α : Type u_2<VAR>One α<GOAL>Set.toFinset 1 = 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>Set.toFinset 0 = 0
<VAR>α : Type u_2<VAR>One α<VAR>h : Set.Finite 1 := ⋯<GOAL>Set.Finite.toFinset h = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>h : Set.Finite 0 := ⋯<GOAL>Set.Finite.toFinset h = 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(s * t)<GOAL>(s * t).toFinset = s.toFinset * t.toFinset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(s + t)<GOAL>(s + t).toFinset = s.toFinset + t.toFinset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hf : (s + t).Finite := ⋯<GOAL>Set.Finite.toFinset hf = hs.toFinset + ht.toFinset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hf : (s * t).Finite := ⋯<GOAL>Set.Finite.toFinset hf = hs.toFinset * ht.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>DecidableEq β<VAR>s : Set α<VAR>t : Set β<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(s +ᵥ t)<GOAL>(s +ᵥ t).toFinset = s.toFinset +ᵥ t.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>DecidableEq β<VAR>s : Set α<VAR>t : Set β<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(s • t)<GOAL>(s • t).toFinset = s.toFinset • t.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>DecidableEq β<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hf : (s +ᵥ t).Finite := ⋯<GOAL>Set.Finite.toFinset hf = hs.toFinset +ᵥ ht.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>DecidableEq β<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hf : (s • t).Finite := ⋯<GOAL>Set.Finite.toFinset hf = hs.toFinset • ht.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>a : α<VAR>s : Set β<VAR>Fintype ↑s<VAR>Fintype ↑(a +ᵥ s)<GOAL>(a +ᵥ s).toFinset = a +ᵥ s.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>a : α<VAR>s : Set β<VAR>Fintype ↑s<VAR>Fintype ↑(a • s)<GOAL>(a • s).toFinset = a • s.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>a : α<VAR>s : Set β<VAR>hs : s.Finite<VAR>hf : (a +ᵥ s).Finite := ⋯<GOAL>Set.Finite.toFinset hf = a +ᵥ hs.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>a : α<VAR>s : Set β<VAR>hs : s.Finite<VAR>hf : (a • s).Finite := ⋯<GOAL>Set.Finite.toFinset hf = a • hs.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>VSub α β<VAR>s t : Set β<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(s -ᵥ t)<GOAL>(s -ᵥ t).toFinset = s.toFinset -ᵥ t.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>VSub α β<VAR>s t : Set β<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hf : (s -ᵥ t).Finite := ⋯<GOAL>Set.Finite.toFinset hf = hs.toFinset -ᵥ ht.toFinset
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>s : Set β<GOAL>Nat.card ↑(a +ᵥ s) = Nat.card ↑s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>a : α<VAR>s : Set β<GOAL>Nat.card ↑(a • s) = Nat.card ↑s
<VAR>α : Type u_2<VAR>Add α<VAR>IsCancelAdd α<VAR>s t : Set α<GOAL>Nat.card ↑(s + t) ≤ Nat.card ↑s * Nat.card ↑t
<VAR>α : Type u_2<VAR>Mul α<VAR>IsCancelMul α<VAR>s t : Set α<GOAL>Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s : Set α<GOAL>Nat.card ↑s⁻¹ = Nat.card ↑s
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s : Set α<GOAL>Nat.card ↑(-s) = Nat.card ↑s
<VAR>α : Type u_2<VAR>AddGroup α<VAR>s t : Set α<GOAL>Nat.card ↑(s - t) ≤ Nat.card ↑s * Nat.card ↑t
<VAR>α : Type u_2<VAR>Group α<VAR>s t : Set α<GOAL>Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t
<VAR>α : Type u<VAR>v : Fin 0 → α<GOAL>v = ![]
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<GOAL>(Matrix.vecHead fun x => a) = a
<VAR>α : Type u<VAR>m : ℕ<VAR>x : α<VAR>u : Fin m → α<GOAL>Matrix.vecCons x u 0 = x
<VAR>α : Type u<VAR>m : ℕ<VAR>h : 0 < m.succ<VAR>x : α<VAR>u : Fin m → α<GOAL>Matrix.vecCons x u ⟨0, h⟩ = x
<VAR>α : Type u<VAR>m : ℕ<VAR>x : α<VAR>u : Fin m → α<VAR>i : Fin m<GOAL>Matrix.vecCons x u i.succ = u i
<VAR>α : Type u<VAR>m i : ℕ<VAR>h : i.succ < m.succ<VAR>x : α<VAR>u : Fin m → α<GOAL>Matrix.vecCons x u ⟨i.succ, h⟩ = u ⟨i, ⋯⟩
<VAR>α : Type u<VAR>m : ℕ<VAR>x : α<VAR>u : Fin m → α<GOAL>Matrix.vecHead (Matrix.vecCons x u) = x
<VAR>α : Type u<VAR>m : ℕ<VAR>x : α<VAR>u : Fin m → α<GOAL>Matrix.vecTail (Matrix.vecCons x u) = u
<VAR>α : Type u<VAR>n' : Type u_4<VAR>j : n'<GOAL>(fun i => ![] i j) = ![]
<VAR>α : Type u<VAR>m : ℕ<VAR>u : Fin m.succ → α<GOAL>Matrix.vecCons (Matrix.vecHead u) (Matrix.vecTail u) = u
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>u : Fin n → α<GOAL>Set.range (Matrix.vecCons x u) = {x} ∪ Set.range u
<VAR>α : Type u<VAR>u : Fin 0 → α<GOAL>Set.range u = ∅
<VAR>α : Type u<VAR>x : α<VAR>u : Fin 0 → α<GOAL>Set.range (Matrix.vecCons x u) = {x}
<VAR>α : Type u<VAR>x y : α<VAR>u : Fin 0 → α<GOAL>Set.range (Matrix.vecCons x (Matrix.vecCons y u)) = {x, y}
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<GOAL>(Matrix.vecCons a fun x => a) = fun x => a
<VAR>α : Type u<VAR>a : α<GOAL>![a] = fun x => a
<VAR>α : Type u<VAR>m : ℕ<VAR>x : α<VAR>u : Fin m.succ → α<GOAL>Matrix.vecCons x u 1 = Matrix.vecHead u
<VAR>α : Type u<VAR>m : ℕ<VAR>x : α<VAR>u : Fin m.succ.succ → α<GOAL>Matrix.vecCons x u 2 = Matrix.vecHead (Matrix.vecTail u)
<VAR>α : Type u<VAR>m : ℕ<VAR>x : α<VAR>u : Fin m.succ.succ.succ → α<GOAL>Matrix.vecCons x u 3 = Matrix.vecHead (Matrix.vecTail (Matrix.vecTail u))
<VAR>α : Type u<VAR>m : ℕ<VAR>x : α<VAR>u : Fin m.succ.succ.succ.succ → α<GOAL>Matrix.vecCons x u 4 = Matrix.vecHead (Matrix.vecTail (Matrix.vecTail (Matrix.vecTail u)))
<VAR>α : Type u<VAR>x : α<VAR>u : Fin 0 → α<VAR>i : Fin 1<GOAL>Matrix.vecCons x u i = x
<VAR>α : Type u<VAR>x : α<VAR>u : Fin 0 → α<GOAL>Matrix.vecCons x u = fun x_1 => x
<VAR>m n : ℕ<VAR>α : Type u_4<VAR>o : ℕ<VAR>ho : o = m + n<VAR>u : Fin m → α<VAR>v : Fin n → α<GOAL>Matrix.vecAppend ho u v = fun i => if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩
<VAR>m n : ℕ<VAR>α : Type u_4<VAR>o : ℕ<VAR>ho : o + 1 = m + 1 + n<VAR>u : Fin (m + 1) → α<VAR>v : Fin n → α<GOAL>Matrix.vecAppend ho u v 0 = u 0
<VAR>α : Type u<VAR>n : ℕ<VAR>v : Fin n → α<GOAL>Matrix.vecAppend ⋯ ![] v = v
<VAR>α : Type u<VAR>m n o : ℕ<VAR>ho : o + 1 = m + 1 + n<VAR>x : α<VAR>u : Fin m → α<VAR>v : Fin n → α<GOAL>Matrix.vecAppend ho (Matrix.vecCons x u) v = Matrix.vecCons x (Matrix.vecAppend ⋯ u v)
<VAR>α : Type u<VAR>n : ℕ<VAR>v : Fin n → α<GOAL>Matrix.vecAlt0 ⋯ (Matrix.vecAppend ⋯ v v) = v ∘ fun n_1 => n_1 + n_1
<VAR>α : Type u<VAR>n : ℕ<VAR>v : Fin (n + 1) → α<GOAL>Matrix.vecAlt1 ⋯ (Matrix.vecAppend ⋯ v v) = v ∘ fun n_1 => n_1 + n_1 + 1
<VAR>α : Type u<VAR>m n : ℕ<VAR>hm : m + 2 = n + 1 + (n + 1)<VAR>v : Fin (m + 2) → α<GOAL>Matrix.vecHead (Matrix.vecAlt0 hm v) = v 0
<VAR>α : Type u<VAR>m n : ℕ<VAR>hm : m + 2 = n + 1 + (n + 1)<VAR>v : Fin (m + 2) → α<GOAL>Matrix.vecHead (Matrix.vecAlt1 hm v) = v 1
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>u : Fin n → α<VAR>i : Fin (n + 1)<GOAL>Matrix.vecCons x u (i + i) = Matrix.vecAlt0 ⋯ (Matrix.vecAppend ⋯ (Matrix.vecCons x u) (Matrix.vecCons x u)) i
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>u : Fin n → α<VAR>i : Fin (n + 1)<GOAL>Matrix.vecCons x u (i + i + 1) = Matrix.vecAlt1 ⋯ (Matrix.vecAppend ⋯ (Matrix.vecCons x u) (Matrix.vecCons x u)) i
<VAR>α : Type u<VAR>m n : ℕ<VAR>h : m + 1 + 1 = n + 1 + (n + 1)<VAR>x y : α<VAR>u : Fin m → α<GOAL>Matrix.vecAlt0 h (Matrix.vecCons x (Matrix.vecCons y u)) = Matrix.vecCons x (Matrix.vecAlt0 ⋯ u)
<VAR>α : Type u_4<VAR>h : 0 = 0 + 0<GOAL>Matrix.vecAlt0 h ![] = ![]
<VAR>α : Type u<VAR>m n : ℕ<VAR>h : m + 1 + 1 = n + 1 + (n + 1)<VAR>x y : α<VAR>u : Fin m → α<GOAL>Matrix.vecAlt1 h (Matrix.vecCons x (Matrix.vecCons y u)) = Matrix.vecCons y (Matrix.vecAlt1 ⋯ u)
<VAR>α : Type u_4<VAR>h : 0 = 0 + 0<GOAL>Matrix.vecAlt1 h ![] = ![]
<VAR>α : Type u<VAR>x : α<GOAL>(fun x_1 => x) = ![x]
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M N : Matrix m n α<GOAL>(∀ (i : m) (j : n), M i j = N i j) ↔ M = N
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M N : Matrix m n α<GOAL>(∀ (i : m) (j : n), M i j = N i j) → M = N
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>f : m → n → α<VAR>i : m<VAR>j : n<GOAL>Matrix.of f i j = f i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>f : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>Matrix.of.symm f i j = f i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>M : Matrix m n α<VAR>f : α → β<VAR>i : m<VAR>j : n<GOAL>M.map f i j = f (M i j)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<GOAL>M.map id = M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<GOAL>(M.map fun x => x) = M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>β : Type u_10<VAR>γ : Type u_11<VAR>f : α → β<VAR>g : β → γ<GOAL>(M.map f).map g = M.map (g ∘ f)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Injective fun M => M.map f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>i : n<VAR>j : m<GOAL>Mᵀ i j = M j i
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Zero α<VAR>i : m<VAR>j : n<GOAL>0 i j = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Add α<VAR>A B : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(A + B) i j = A i j + B i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>SMul β α<VAR>r : β<VAR>A : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(r • A) i j = r • A i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Sub α<VAR>A B : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(A - B) i j = A i j - B i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Neg α<VAR>A : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(-A) i j = -A i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Zero α<GOAL>Matrix.of 0 = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Add α<VAR>f g : m → n → α<GOAL>Matrix.of f + Matrix.of g = Matrix.of (f + g)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Sub α<VAR>f g : m → n → α<GOAL>Matrix.of f - Matrix.of g = Matrix.of (f - g)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Neg α<VAR>f : m → n → α<GOAL>-Matrix.of f = Matrix.of (-f)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>SMul R α<VAR>r : R<VAR>f : m → n → α<GOAL>r • Matrix.of f = Matrix.of (r • f)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>Zero α<VAR>Zero β<VAR>f : α → β<VAR>h : f 0 = 0<GOAL>Matrix.map 0 f = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>Add α<VAR>Add β<VAR>f : α → β<VAR>hf : ∀ (a₁ a₂ : α), f (a₁ + a₂) = f a₁ + f a₂<VAR>M N : Matrix m n α<GOAL>(M + N).map f = M.map f + N.map f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>Sub α<VAR>Sub β<VAR>f : α → β<VAR>hf : ∀ (a₁ a₂ : α), f (a₁ - a₂) = f a₁ - f a₂<VAR>M N : Matrix m n α<GOAL>(M - N).map f = M.map f - N.map f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>SMul R α<VAR>SMul R β<VAR>f : α → β<VAR>r : R<VAR>hf : ∀ (a : α), f (r • a) = r • f a<VAR>M : Matrix m n α<GOAL>(r • M).map f = r • M.map f
<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>Mul α<VAR>Mul β<VAR>f : α → β<VAR>r : α<VAR>A : Matrix n n α<VAR>hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂<GOAL>(r • A).map f = f r • A.map f
<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>Mul α<VAR>Mul β<VAR>f : α → β<VAR>r : α<VAR>A : Matrix n n α<VAR>hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂<GOAL>(MulOpposite.op r • A).map f = MulOpposite.op (f r) • A.map f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>S : Type u_8<VAR>SMul R S<VAR>k : R<VAR>hk : IsSMulRegular S k<GOAL>IsSMulRegular (Matrix m n S) k
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Mul α<VAR>k : α<VAR>hk : IsLeftRegular k<GOAL>IsSMulRegular (Matrix m n α) k
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>d : n → α<VAR>i j : n<GOAL>Matrix.diagonal d i j = if i = j then d i else 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>d : n → α<VAR>i : n<GOAL>Matrix.diagonal d i i = d i
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>d : n → α<VAR>i j : n<VAR>h : i ≠ j<GOAL>Matrix.diagonal d i j = 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>d : n → α<VAR>i j : n<VAR>h : j ≠ i<GOAL>Matrix.diagonal d i j = 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>d₁ d₂ : n → α<GOAL>Matrix.diagonal d₁ = Matrix.diagonal d₂ ↔ ∀ (i : n), d₁ i = d₂ i
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<GOAL>Function.Injective Matrix.diagonal
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<GOAL>(Matrix.diagonal fun x => 0) = 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>v : n → α<GOAL>(Matrix.diagonal v)ᵀ = Matrix.diagonal v
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddZeroClass α<VAR>d₁ d₂ : n → α<GOAL>Matrix.diagonal d₁ + Matrix.diagonal d₂ = Matrix.diagonal fun i => d₁ i + d₂ i
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>SMulZeroClass R α<VAR>r : R<VAR>d : n → α<GOAL>Matrix.diagonal (r • d) = r • Matrix.diagonal d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>NegZeroClass α<VAR>d : n → α<GOAL>-Matrix.diagonal d = Matrix.diagonal fun i => -d i
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>SubNegZeroMonoid α<VAR>d₁ d₂ : n → α<GOAL>Matrix.diagonal d₁ - Matrix.diagonal d₂ = Matrix.diagonal fun i => d₁ i - d₂ i
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>NatCast α<VAR>m : ℕ<GOAL>(Matrix.diagonal fun x => ↑m) = ↑m
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>NatCast α<VAR>m : ℕ<GOAL>Matrix.diagonal ↑m = ↑m
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>NatCast α<VAR>m : ℕ<VAR>m.AtLeastTwo<GOAL>(Matrix.diagonal fun x => OfNat.ofNat m) = OfNat.ofNat m
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>NatCast α<VAR>m : ℕ<VAR>m.AtLeastTwo<GOAL>Matrix.diagonal (OfNat.ofNat m) = OfNat.ofNat m
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>IntCast α<VAR>m : ℤ<GOAL>(Matrix.diagonal fun x => ↑m) = ↑m
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>IntCast α<VAR>m : ℤ<GOAL>Matrix.diagonal ↑m = ↑m
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddZeroClass α<VAR>d : n → α<GOAL>(Matrix.diagonalAddMonoidHom n α) d = Matrix.diagonal d
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>DecidableEq n<VAR>Semiring R<VAR>AddCommMonoid α<VAR>Module R α<GOAL>∀ (a : n → α), (Matrix.diagonalLinearMap n R α) a = (↑(Matrix.diagonalAddMonoidHom n α)).toFun a
<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>DecidableEq n<VAR>Zero α<VAR>Zero β<VAR>f : α → β<VAR>h : f 0 = 0<VAR>d : n → α<GOAL>(Matrix.diagonal d).map f = Matrix.diagonal fun m => f (d m)
<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>DecidableEq n<VAR>AddMonoidWithOne α<VAR>AddMonoidWithOne β<VAR>f : α → β<VAR>h : f 0 = 0<VAR>d : ℕ<GOAL>(↑d).map f = Matrix.diagonal fun x => f ↑d
<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>DecidableEq n<VAR>AddMonoidWithOne α<VAR>AddMonoidWithOne β<VAR>f : α → β<VAR>h : f 0 = 0<VAR>d : ℕ<VAR>d.AtLeastTwo<GOAL>(OfNat.ofNat d).map f = Matrix.diagonal fun x => f (OfNat.ofNat d)
<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>DecidableEq n<VAR>AddGroupWithOne α<VAR>AddGroupWithOne β<VAR>f : α → β<VAR>h : f 0 = 0<VAR>d : ℤ<GOAL>(↑d).map f = Matrix.diagonal fun x => f ↑d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>v : n → α<GOAL>(Matrix.diagonal v)ᴴ = Matrix.diagonal (star v)
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<GOAL>(Matrix.diagonal fun x => 1) = 1
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>i j : n<GOAL>1 i j = if i = j then 1 else 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>i : n<GOAL>1 i i = 1
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>i j : n<GOAL>i ≠ j → 1 i j = 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>i j : n<GOAL>j ≠ i → 1 i j = 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>Zero β<VAR>One β<VAR>f : α → β<VAR>h₀ : f 0 = 0<VAR>h₁ : f 1 = 1<GOAL>Matrix.map 1 f = 1
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>i j : n<GOAL>1 i j = Pi.single i 1 j
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>Preorder α<VAR>ZeroLEOneClass α<VAR>i j : n<GOAL>0 ≤ 1 i j
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>Preorder α<VAR>ZeroLEOneClass α<VAR>i : n<GOAL>0 ≤ 1 i
<VAR>n : Type u_3<VAR>α : Type v<VAR>A : Matrix n n α<VAR>i : n<GOAL>A.diag i = A i i
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>a : n → α<GOAL>(Matrix.diagonal a).diag = a
<VAR>n : Type u_3<VAR>α : Type v<VAR>A : Matrix n n α<GOAL>Aᵀ.diag = A.diag
<VAR>n : Type u_3<VAR>α : Type v<VAR>Zero α<GOAL>Matrix.diag 0 = 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>Add α<VAR>A B : Matrix n n α<GOAL>(A + B).diag = A.diag + B.diag
<VAR>n : Type u_3<VAR>α : Type v<VAR>Sub α<VAR>A B : Matrix n n α<GOAL>(A - B).diag = A.diag - B.diag
<VAR>n : Type u_3<VAR>α : Type v<VAR>Neg α<VAR>A : Matrix n n α<GOAL>(-A).diag = -A.diag
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>SMul R α<VAR>r : R<VAR>A : Matrix n n α<GOAL>(r • A).diag = r • A.diag
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<GOAL>Matrix.diag 1 = 1
<VAR>n : Type u_3<VAR>α : Type v<VAR>AddZeroClass α<VAR>A : Matrix n n α<VAR>i : n<GOAL>(Matrix.diagAddMonoidHom n α) A i = A.diag i
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Semiring R<VAR>AddCommMonoid α<VAR>Module R α<GOAL>∀ (a : Matrix n n α) (a_1 : n), (Matrix.diagLinearMap n R α) a a_1 = (↑(Matrix.diagAddMonoidHom n α)).toFun a a_1
<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>f : α → β<VAR>A : Matrix n n α<GOAL>(A.map f).diag = f ∘ A.diag
<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>A : Matrix n n α<GOAL>Aᴴ.diag = star A.diag
<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>l : List (Matrix n n α)<GOAL>l.sum.diag = (List.map Matrix.diag l).sum
<VAR>n : Type u_3<VAR>α : Type v<VAR>AddCommMonoid α<VAR>s : Multiset (Matrix n n α)<GOAL>s.sum.diag = (Multiset.map Matrix.diag s).sum
<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_10<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>f : ι → Matrix n n α<GOAL>(∑ i ∈ s, f i).diag = ∑ i ∈ s, (f i).diag
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype m<VAR>Fintype n<VAR>NonUnitalSemiring α<VAR>u : m → α<VAR>w : n → α<VAR>v : Matrix m n α<GOAL>(fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>AddCommMonoid α<VAR>CommSemigroup α<VAR>v w : m → α<GOAL>v ⬝ᵥ w = w ⬝ᵥ v
<VAR>α : Type v<VAR>AddCommMonoid α<VAR>Mul α<VAR>v w : PUnit.{u_10 + 1} → α<GOAL>v ⬝ᵥ w = v PUnit.unit * w PUnit.unit
<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype n<VAR>MulOneClass α<VAR>AddCommMonoid α<VAR>v : n → α<GOAL>v ⬝ᵥ 1 = ∑ i : n, v i
<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype n<VAR>MulOneClass α<VAR>AddCommMonoid α<VAR>v : n → α<GOAL>1 ⬝ᵥ v = ∑ i : n, v i
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>v : m → α<GOAL>v ⬝ᵥ 0 = 0
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>v : m → α<GOAL>(v ⬝ᵥ fun x => 0) = 0
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>v : m → α<GOAL>0 ⬝ᵥ v = 0
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>v : m → α<GOAL>(fun x => 0) ⬝ᵥ v = 0
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>u v w : m → α<GOAL>(u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>u v w : m → α<GOAL>u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype m<VAR>Fintype n<VAR>NonUnitalNonAssocSemiring α<VAR>u v : m → α<VAR>x y : n → α<GOAL>Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype m<VAR>Fintype n<VAR>NonUnitalNonAssocSemiring α<VAR>u : m → α<VAR>x : n → α<VAR>e : m ≃ n<GOAL>u ∘ ⇑e.symm ⬝ᵥ x = u ⬝ᵥ x ∘ ⇑e
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype m<VAR>Fintype n<VAR>NonUnitalNonAssocSemiring α<VAR>u : m → α<VAR>x : n → α<VAR>e : n ≃ m<GOAL>u ⬝ᵥ x ∘ ⇑e.symm = u ∘ ⇑e ⬝ᵥ x
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype m<VAR>Fintype n<VAR>NonUnitalNonAssocSemiring α<VAR>x y : n → α<VAR>e : m ≃ n<GOAL>x ∘ ⇑e ⬝ᵥ y ∘ ⇑e = x ⬝ᵥ y
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>NonUnitalNonAssocSemiring α<VAR>v w : m → α<VAR>i : m<GOAL>Matrix.diagonal v i ⬝ᵥ w = v i * w i