ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>M₁ : Submodule R M<VAR>N₁ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<GOAL>∃ N', ∃ (hN : N' ≤ N₁), Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M₁) (Submodule.inclusion hN)))
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Preorder ι<VAR>G : ι → Type u_3<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ι<VAR>g : G i<VAR>m : M<GOAL>(TensorProduct.fromDirectLimit f M) ((Module.DirectLimit.of R ι (fun x => G x ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)) = (Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Preorder ι<VAR>G : ι → Type u_3<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ι<VAR>g : G i<VAR>m : M<GOAL>(TensorProduct.toDirectLimit f M) ((Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m) = (Module.DirectLimit.of R ι (fun x => G x ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Preorder ι<VAR>G : ι → Type u_3<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>g : G i<VAR>m : M<GOAL>(TensorProduct.directLimitLeft f M) ((Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m) = (Module.DirectLimit.of R ι (fun i => G i ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Preorder ι<VAR>G : ι → Type u_3<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>g : G i<VAR>m : M<GOAL>(TensorProduct.directLimitLeft f M).symm ((Module.DirectLimit.of R ι (fun x => G x ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)) = (Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Preorder ι<VAR>G : ι → Type u_3<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>m : M<VAR>g : G i<GOAL>(TensorProduct.directLimitRight f M) (m ⊗ₜ[R] (Module.DirectLimit.of R ι G f i) g) = (Module.DirectLimit.of R ι (fun x => M ⊗[R] G x) (fun i j h => LinearMap.lTensor M (f i j h)) i) (m ⊗ₜ[R] g)
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Preorder ι<VAR>G : ι → Type u_3<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>m : M<VAR>g : G i<GOAL>(TensorProduct.directLimitRight f M).symm ((Module.DirectLimit.of R ι (fun x => M ⊗[R] G x) (fun i j h => LinearMap.lTensor M (f i j h)) i) (m ⊗ₜ[R] g)) = m ⊗ₜ[R] (Module.DirectLimit.of R ι G f i) g
<VAR>n : Type u_1<VAR>m : Type u_2<VAR>Fintype n<VAR>DecidableEq n<VAR>Fintype m<VAR>DecidableEq m<VAR>R : Type u_3<VAR>Semiring R<VAR>InvariantBasisNumber R<VAR>M : Matrix n m R<VAR>N : Matrix m n R<VAR>h : M * N = 1<VAR>h' : N * M = 1<GOAL>Fintype.card n = Fintype.card m
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i : ι<VAR>b : φ i<GOAL>(LinearMap.stdBasis R φ i) b = Function.update 0 i b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>DecidableEq ι<VAR>i i' : ι<GOAL>(LinearMap.stdBasis R (fun _x => R) i) 1 i' = if i = i' then 1 else 0
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>⇑(LinearMap.stdBasis R φ i) = Pi.single i
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i : ι<VAR>b : φ i<GOAL>(LinearMap.stdBasis R φ i) b i = b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : j ≠ i<VAR>b : φ i<GOAL>(LinearMap.stdBasis R φ i) b j = 0
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>LinearMap.stdBasis R φ i = LinearMap.pi (LinearMap.diag i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>LinearMap.ker (LinearMap.stdBasis R φ i) = ⊥
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i j : ι<GOAL>LinearMap.proj i ∘ₗ LinearMap.stdBasis R φ j = LinearMap.diag j i
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>LinearMap.proj i ∘ₗ LinearMap.stdBasis R φ i = LinearMap.id
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<GOAL>LinearMap.proj i ∘ₗ LinearMap.stdBasis R φ j = 0
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<GOAL>⨆ i ∈ I, LinearMap.range (LinearMap.stdBasis R φ i) ≤ ⨅ i ∈ J, LinearMap.ker (LinearMap.proj i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>I : Finset ι<VAR>J : Set ι<VAR>hu : Set.univ ⊆ ↑I ∪ J<GOAL>⨅ i ∈ J, LinearMap.ker (LinearMap.proj i) ≤ ⨆ i ∈ I, LinearMap.range (LinearMap.stdBasis R φ i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>I J : Set ι<VAR>hd : Disjoint I J<VAR>hu : Set.univ ⊆ I ∪ J<VAR>hI : I.Finite<GOAL>⨆ i ∈ I, LinearMap.range (LinearMap.stdBasis R φ i) = ⨅ i ∈ J, LinearMap.ker (LinearMap.proj i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>Finite ι<GOAL>⨆ i, LinearMap.range (LinearMap.stdBasis R φ i) = ⊤
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>φ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<GOAL>Disjoint (⨆ i ∈ I, LinearMap.range (LinearMap.stdBasis R φ i)) (⨆ i ∈ J, LinearMap.range (LinearMap.stdBasis R φ i))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>Semiring R<VAR>DecidableEq ι<VAR>a : R<GOAL>(fun i => (LinearMap.stdBasis R (fun x => R) i) a) = fun i => ⇑(Finsupp.single i a)
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>Ring R<VAR>(i : η) → AddCommGroup (Ms i)<VAR>(i : η) → Module R (Ms i)<VAR>DecidableEq η<VAR>v : (j : η) → ιs j → Ms j<VAR>hs : ∀ (i : η), LinearIndependent R (v i)<GOAL>LinearIndependent R fun ji => (LinearMap.stdBasis R Ms ji.fst) (v ji.fst ji.snd)
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>Semiring R<VAR>(i : η) → AddCommMonoid (Ms i)<VAR>(i : η) → Module R (Ms i)<VAR>Fintype η<VAR>DecidableEq η<VAR>s : (j : η) → Basis (ιs j) R (Ms j)<VAR>j : η<VAR>i : ιs j<GOAL>(Pi.basis s).repr ((LinearMap.stdBasis R Ms j) ((s j) i)) = Finsupp.single ⟨j, i⟩ 1
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>Semiring R<VAR>(i : η) → AddCommMonoid (Ms i)<VAR>(i : η) → Module R (Ms i)<VAR>Fintype η<VAR>DecidableEq η<VAR>s : (j : η) → Basis (ιs j) R (Ms j)<VAR>ji : (j : η) × ιs j<GOAL>(Pi.basis s) ji = (LinearMap.stdBasis R Ms ji.fst) ((s ji.fst) ji.snd)
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>Semiring R<VAR>(i : η) → AddCommMonoid (Ms i)<VAR>(i : η) → Module R (Ms i)<VAR>Fintype η<VAR>s : (j : η) → Basis (ιs j) R (Ms j)<VAR>x : (j : η) → Ms j<VAR>ji : (j : η) × ιs j<GOAL>((Pi.basis s).repr x) ji = ((s ji.fst).repr (x ji.fst)) ji.snd
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>Semiring R<VAR>Finite η<VAR>DecidableEq η<VAR>i : η<GOAL>(Pi.basisFun R η) i = (LinearMap.stdBasis R (fun x => R) i) 1
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>Semiring R<VAR>Finite η<VAR>x : η → R<VAR>i : η<GOAL>((Pi.basisFun R η).repr x) i = x i
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>Semiring R<VAR>Finite η<GOAL>(Pi.basisFun R η).equivFun = LinearEquiv.refl R (η → R)
<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>M : Type u_7<VAR>Fintype ι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : ι → M<VAR>w : ι → R<GOAL>((Module.piEquiv ι R M) v) w = ∑ i : ι, w i • v i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Finite ι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : ι → M<GOAL>LinearMap.range ((Module.piEquiv ι R M) v) = Submodule.span R (Set.range v)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Finite ι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : ι → M<GOAL>Function.Surjective ⇑((Module.piEquiv ι R M) v) ↔ Submodule.span R (Set.range v) = ⊤
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>Fintype m<VAR>Finite n<VAR>Semiring R<VAR>i : m<VAR>j : n<VAR>DecidableEq m<VAR>DecidableEq n<GOAL>(Matrix.stdBasis R m n) (i, j) = Matrix.stdBasisMatrix i j 1
<VAR>R : Type u_6<VAR>AddCommMonoid R<VAR>o : Type u_8<VAR>Fintype o<VAR>DecidableEq o<VAR>d : o → R<GOAL>(Matrix.diagonal d).trace = ∑ i : o, d i
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<GOAL>Matrix.trace 0 = 0
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>IsEmpty n<VAR>A : Matrix n n R<GOAL>A.trace = 0
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>A B : Matrix n n R<GOAL>(A + B).trace = A.trace + B.trace
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>Monoid α<VAR>DistribMulAction α R<VAR>r : α<VAR>A : Matrix n n R<GOAL>(r • A).trace = r • A.trace
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>A : Matrix n n R<GOAL>Aᵀ.trace = A.trace
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>StarAddMonoid R<VAR>A : Matrix n n R<GOAL>Aᴴ.trace = star A.trace
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>A : Matrix n n R<GOAL>(Matrix.traceAddMonoidHom n R) A = A.trace
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>Semiring α<VAR>Module α R<VAR>A : Matrix n n R<GOAL>(Matrix.traceLinearMap n α R) A = A.trace
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>l : List (Matrix n n R)<GOAL>l.sum.trace = (List.map Matrix.trace l).sum
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>s : Multiset (Matrix n n R)<GOAL>s.sum.trace = (Multiset.map Matrix.trace s).sum
<VAR>ι : Type u_1<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommMonoid R<VAR>s : Finset ι<VAR>f : ι → Matrix n n R<GOAL>(∑ i ∈ s, f i).trace = ∑ i ∈ s, (f i).trace
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>S : Type u_7<VAR>Fintype n<VAR>AddCommMonoid R<VAR>AddCommMonoid S<VAR>f : R →+ S<VAR>A : Matrix n n R<GOAL>f A.trace = (f.mapMatrix A).trace
<VAR>n : Type u_3<VAR>p : Type u_4<VAR>R : Type u_6<VAR>Fintype n<VAR>Fintype p<VAR>AddCommMonoid R<VAR>DecidableEq p<VAR>M : p → Matrix n n R<GOAL>(Matrix.blockDiagonal M).trace = ∑ i : p, (M i).trace
<VAR>p : Type u_4<VAR>R : Type u_6<VAR>Fintype p<VAR>AddCommMonoid R<VAR>DecidableEq p<VAR>m : p → Type u_8<VAR>(i : p) → Fintype (m i)<VAR>M : (i : p) → Matrix (m i) (m i) R<GOAL>(Matrix.blockDiagonal' M).trace = ∑ i : p, (M i).trace
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommGroup R<VAR>A B : Matrix n n R<GOAL>(A - B).trace = A.trace - B.trace
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>AddCommGroup R<VAR>A : Matrix n n R<GOAL>(-A).trace = -A.trace
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>DecidableEq n<VAR>AddCommMonoidWithOne R<GOAL>Matrix.trace 1 = ↑(Fintype.card n)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype m<VAR>Fintype n<VAR>AddCommMonoid R<VAR>Mul R<VAR>A : Matrix m n R<VAR>B : Matrix n m R<GOAL>(Aᵀ * Bᵀ).trace = (A * B).trace
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype m<VAR>Fintype n<VAR>AddCommMonoid R<VAR>CommSemigroup R<VAR>A : Matrix m n R<VAR>B : Matrix n m R<GOAL>(A * B).trace = (B * A).trace
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>R : Type u_6<VAR>Fintype m<VAR>Fintype n<VAR>Fintype p<VAR>NonUnitalCommSemiring R<VAR>A : Matrix m n R<VAR>B : Matrix n p R<VAR>C : Matrix p m R<GOAL>(A * B * C).trace = (C * A * B).trace
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>R : Type u_6<VAR>Fintype m<VAR>Fintype n<VAR>Fintype p<VAR>NonUnitalCommSemiring R<VAR>A : Matrix m n R<VAR>B : Matrix n p R<VAR>C : Matrix p m R<GOAL>(A * (B * C)).trace = (C * (A * B)).trace
<VAR>n : Type u_3<VAR>R : Type u_6<VAR>Fintype n<VAR>ι : Type u_8<VAR>Unique ι<VAR>NonUnitalNonAssocSemiring R<VAR>a b : n → R<GOAL>(Matrix.col ι a * Matrix.row ι b).trace = a ⬝ᵥ b
<VAR>R : Type u_6<VAR>n : ℕ<VAR>NonUnitalNonAssocSemiring R<VAR>M : Matrix (Fin n.succ) (Fin n.succ) R<GOAL>M 0 0 + (M.submatrix Fin.succ Fin.succ).trace = M.trace
<VAR>R : Type u_6<VAR>AddCommMonoid R<VAR>A : Matrix (Fin 0) (Fin 0) R<GOAL>A.trace = 0
<VAR>R : Type u_6<VAR>AddCommMonoid R<VAR>A : Matrix (Fin 1) (Fin 1) R<GOAL>A.trace = A 0 0
<VAR>R : Type u_6<VAR>AddCommMonoid R<VAR>A : Matrix (Fin 2) (Fin 2) R<GOAL>A.trace = A 0 0 + A 1 1
<VAR>R : Type u_6<VAR>AddCommMonoid R<VAR>A : Matrix (Fin 3) (Fin 3) R<GOAL>A.trace = A 0 0 + A 1 1 + A 2 2
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>A : Matrix n n α<VAR>h : A.IsSymm<GOAL>A.transpose = A
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>A : Matrix n n α<GOAL>A.IsSymm ↔ ∀ (i j : n), A j i = A i j
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>A : Matrix n n α<GOAL>(∀ (i j : n), A j i = A i j) → A.IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>A : Matrix n n α<VAR>h : A.IsSymm<VAR>i j : n<GOAL>A j i = A i j
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>Fintype n<VAR>CommSemiring α<VAR>A : Matrix n n α<GOAL>(A * A.transpose).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>Fintype n<VAR>CommSemiring α<VAR>A : Matrix n n α<GOAL>(A.transpose * A).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>AddCommSemigroup α<VAR>A : Matrix n n α<GOAL>(A + A.transpose).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>AddCommSemigroup α<VAR>A : Matrix n n α<GOAL>(A.transpose + A).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>Zero α<GOAL>Matrix.IsSymm 0
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>DecidableEq n<VAR>Zero α<VAR>One α<GOAL>Matrix.IsSymm 1
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>CommSemiring α<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n α<VAR>h : A.IsSymm<VAR>k : ℕ<GOAL>(A ^ k).IsSymm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_3<VAR>A : Matrix n n α<VAR>h : A.IsSymm<VAR>f : α → β<GOAL>(A.map f).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>A : Matrix n n α<VAR>h : A.IsSymm<GOAL>A.transpose.IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>Star α<VAR>A : Matrix n n α<VAR>h : A.IsSymm<GOAL>A.conjTranspose.IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>Neg α<VAR>A : Matrix n n α<VAR>h : A.IsSymm<GOAL>(-A).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>A B : Matrix n n α<VAR>Add α<VAR>hA : A.IsSymm<VAR>hB : B.IsSymm<GOAL>(A + B).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>A B : Matrix n n α<VAR>Sub α<VAR>hA : A.IsSymm<VAR>hB : B.IsSymm<GOAL>(A - B).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>R : Type u_5<VAR>SMul R α<VAR>A : Matrix n n α<VAR>h : A.IsSymm<VAR>k : R<GOAL>(k • A).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>m : Type u_4<VAR>A : Matrix n n α<VAR>h : A.IsSymm<VAR>f : m → n<GOAL>(A.submatrix f f).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>DecidableEq n<VAR>Zero α<VAR>v : n → α<GOAL>(Matrix.diagonal v).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>m : Type u_4<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>hA : A.IsSymm<VAR>hBC : B.transpose = C<VAR>hD : D.IsSymm<GOAL>(Matrix.fromBlocks A B C D).IsSymm
<VAR>α : Type u_1<VAR>n : Type u_3<VAR>m : Type u_4<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<GOAL>(Matrix.fromBlocks A B C D).IsSymm ↔ A.IsSymm ∧ B.transpose = C ∧ C.transpose = B ∧ D.IsSymm
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : s.Finite<GOAL>FiniteDimensional k ↥(vectorSpan k s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : s.Finite<GOAL>FiniteDimensional k ↥(affineSpan k s).direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>FiniteDimensional k V<VAR>p : ι → P<VAR>hi : AffineIndependent k p<GOAL>Finite ι
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>FiniteDimensional k V<VAR>s : Set ι<VAR>f : ↑s → P<VAR>hi : AffineIndependent k f<GOAL>s.Finite
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>DecidableEq P<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>s : Finset ι<VAR>n : ℕ<VAR>hc : s.card = n + 1<GOAL>FiniteDimensional.finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 1<GOAL>FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) = n
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>Nonempty ι<VAR>p : ι → P<VAR>hi : AffineIndependent k p<GOAL>FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>FiniteDimensional k V<VAR>Fintype ι<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>hc : Fintype.card ι = FiniteDimensional.finrank k V + 1<GOAL>vectorSpan k (Set.range p) = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>DecidableEq P<VAR>p : ι → P<VAR>s : Finset ι<VAR>n : ℕ<VAR>hc : s.card = n + 1<GOAL>FiniteDimensional.finrank k ↥(vectorSpan k ↑(Finset.image p s)) ≤ n
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p : ι → P<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 1<GOAL>FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) ≤ n
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>Nonempty ι<VAR>p : ι → P<GOAL>FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) + 1 ≤ Fintype.card ι
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p : ι → P<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 1<GOAL>AffineIndependent k p ↔ FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) = n
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p : ι → P<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 1<GOAL>AffineIndependent k p ↔ n ≤ FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p : ι → P<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 2<GOAL>AffineIndependent k p ↔ ¬FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) ≤ n
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p : ι → P<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 2<GOAL>FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) ≤ n ↔ ¬AffineIndependent k p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p : ι → P<VAR>hp : AffineIndependent k p<GOAL>Fintype.card ι ≤ FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<GOAL>s.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<GOAL>s.card < t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>DecidableEq P<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>s : Finset ι<VAR>sm : Submodule k V<VAR>FiniteDimensional k ↥sm<VAR>hle : vectorSpan k ↑(Finset.image p s) ≤ sm<VAR>hc : s.card = FiniteDimensional.finrank k ↥sm + 1<GOAL>vectorSpan k ↑(Finset.image p s) = sm
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>sm : Submodule k V<VAR>FiniteDimensional k ↥sm<VAR>hle : vectorSpan k (Set.range p) ≤ sm<VAR>hc : Fintype.card ι = FiniteDimensional.finrank k ↥sm + 1<GOAL>vectorSpan k (Set.range p) = sm
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>DecidableEq P<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>s : Finset ι<VAR>sp : AffineSubspace k P<VAR>FiniteDimensional k ↥sp.direction<VAR>hle : affineSpan k ↑(Finset.image p s) ≤ sp<VAR>hc : s.card = FiniteDimensional.finrank k ↥sp.direction + 1<GOAL>affineSpan k ↑(Finset.image p s) = sp
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>sp : AffineSubspace k P<VAR>FiniteDimensional k ↥sp.direction<VAR>hle : affineSpan k (Set.range p) ≤ sp<VAR>hc : Fintype.card ι = FiniteDimensional.finrank k ↥sp.direction + 1<GOAL>affineSpan k (Set.range p) = sp
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>FiniteDimensional k V<VAR>Fintype ι<VAR>p : ι → P<VAR>hi : AffineIndependent k p<GOAL>affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = FiniteDimensional.finrank k V + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>FiniteDimensional k V<VAR>n : ℕ<VAR>T : Affine.Simplex k V n<VAR>hrank : FiniteDimensional.finrank k V = n<GOAL>affineSpan k (Set.range T.points) = ⊤