Theorems

A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.

Showing 21-40 of 76

Back Next

The Sum of $n$ Ones is Strictly Increasing in $n$
lemmalem:sum-of-ones-strictly-increasing-2026aAnalysis Algebra
Let $\mathbb{N}$ be the set of natural numbers, with successor map $S$ and order relations $<$ and $\le$ , and for $n\in\mathbb{N}$ let $[n]$ be the initial segment it determines. Let $\mathbb{R}$ be the ordered field of real numbers, with additive identity $0$ and multiplicative…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-04T00:17:33.383707Z
Tuples in a Set
definitiondef:finite-tuple-power-2026aAlgebra Set Theory
Let $X$ be a set, let $n$ be a natural number, and let $[n]$ be the initial segment determined by $n$ , that is, the set of natural numbers $k$ with $1\le k\le n$ . The set $X^{n}$ is the set of all maps from $[n]$ to $X$ . An element $x\in X^{n}$ is called an $n$ -tuple in $X$ ; for…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T01:10:15.970956Z
Dropping a Redundant Vector from a Spanning Family
lemmalem:span-drop-redundant-vector-2026bAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , and let $n$ be a natural number. Inequalities between natural numbers use the order relations on $\mathbb{N}$ . Let $v$ be a tuple in $V^{n+1}$ that spans $V$ , let $j$ be a natural number with $j\le n+1$ , and let $v^{(j)}$ b…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:48:15.998758Z
Extraction of a Summand from a Finite Sum of Vectors
lemmalem:finite-sum-extraction-2026aAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , and let $n$ be a natural number. Inequalities between natural numbers use the order relations on $\mathbb{N}$ . Let $b$ be a tuple in $V^{n+1}$ , with components $b_{k}$ for $1\le k\le n+1$ , and let $j$ be a natural number wi…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:48:12.211615Z
A Linear Subspace is a Vector Space and Inherits an Inner Product
lemmalem:subspace-inner-product-space-2026bAnalysis Algebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ with zero vector $0_{V}$ , and let $W$ be a linear subspace of $V$ . Then the following hold. 1. (Vector space) The set $W$ , equipped with the restrictions to $W$ of the addition and the scalar multiplication of $V$ , is a vect…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:34:38.892784Z
The Span of a Finite Family is the Smallest Subspace Containing It
lemmalem:span-is-subspace-2026bAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$ , let $v\in V^{n}$ be an $n$ -tuple in $V$ with components $v_{k}$ , and let $\operatorname{span}(v)$ be its span. Then the following hold.…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:34:20.469367Z
Finite-Dimensional Vector Space
definitiondef:finite-dimensional-vector-space-2026bAlgebra Linear Algebra
Let $K$ be a field and let $V$ be a vector space over $K$ with zero vector $0_{V}$ . The space $V$ is finite-dimensional if $V=\{0_{V}\}$ , or if there exist a natural number $n$ and an $n$ -tuple $e\in V^{n}$ that is a basis of $V$ .
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:34:14.833470Z
Span of a Finite Family of Vectors
definitiondef:span-finite-family-2026bAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , let $n$ be a natural number, and let $v\in V^{n}$ be an $n$ -tuple in $V$ , with components $v_{k}$ . The span of $v$ is the set…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:34:11.526107Z
Concatenation of Finite Sums
lemmalem:finite-sum-concatenation-2026bAnalysis Algebra
Let $K$ be a field. Let $\mathbb{N}$ be the set of natural numbers, with addition $+$ and successor map $S$ as in that definition, and for a natural number $p$ let $[p]$ be the initial segment determined by $p$ , that is, the set of natural numbers $k$ with $1\le k\le p$ . Let…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:13:48.718428Z
Operations on Linear Operators
definitiondef:operator-operations-2026aAlgebra Linear Algebra
Let $K$ be a field and let $V$ be a vector space over $K$ . The set of linear operators on $V$ carries the following operations, each of which again yields a linear operator on $V$ by Sums, Scalar Multiples, Composites and the Identity are Linear Operators. Let $S$ and $T$ be line…
+0 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T20:21:39.836203Z
Sums, Scalar Multiples, Composites and the Identity are Linear Operators
lemmalem:operator-operations-linear-2026aAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , let $S$ and $T$ be linear operators on $V$ , and let $\lambda\in K$ . Then each of the following maps from $V$ to $V$ is a linear operator on $V$ . 1. (Sum) The map sending $u\in V$ to $S(u)+T(u)$ . 2. (Scalar multiple) The ma…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T20:21:36.186951Z
Linear Operator on a Vector Space
definitiondef:linear-operator-2026aAlgebra Linear Algebra
Let $K$ be a field and let $V$ be a vector space over $K$ . A linear operator on $V$ is a linear map from $V$ to $V$ .
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T20:21:31.809696Z
Standard Basis Vectors of the Complex Coordinate Space
definitiondef:standard-basis-cn-2026aAlgebra Linear Algebra
Let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$ , let $\mathbb{C}^{n}$ be the complex coordinate space, and let $k\in[n]$ . The $k$ -th standard basis vector $e_{k}$ is the element of $\mathbb{C}^{n}$ whose $k$ -th component is $1$ and whose $j$ -th co…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T20:20:00.763293Z
Finite Basis of a Vector Space
definitiondef:finite-basis-2026aAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$ , and let $e:[n]\to V$ be a map with values $e_{k}$ . The family $e$ is a basis of $V$ if it is linearly independent and spans $V$ .
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T20:06:35.458573Z
Finite Family Spanning a Vector Space
definitiondef:spanning-finite-family-2026aAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$ , and let $v:[n]\to V$ be a map with values $v_{k}$ . The family $v$ spans $V$ if for every $u\in V$ there is a map $c:[n]\to K$ with…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T20:05:48.575449Z
Linearly Independent Finite Family
definitiondef:linear-independence-finite-family-2026aAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ with zero vector $0_{V}$ , let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$ , and let $v:[n]\to V$ be a map with values $v_{k}$ . The family $v$ is linearly independent if the only map…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T20:05:45.262532Z
Properties of Finite Sums of Vectors
lemmalem:finite-sum-vector-properties-2026aAlgebra Linear Algebra
Let $K$ be a field and let $V$ be a vector space over $K$ with zero vector $0_{V}$ . Let $\mathbb{N}$ be the set of natural numbers with successor map $S$ as in that definition, ordered by the relation $\le$ of that definition, let $n\in\mathbb{N}$ , and let $[n]$ be the…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T19:51:54.431028Z
Finite Sum Notation in a Vector Space
definitiondef:finite-sum-vector-space-2026aAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ with vector addition $+$ , let $n$ be a natural number with successor map $S$ as in that definition, let $[n]$ be the initial segment determined by $n$ , and let $v:[n]\to V$ be a map, whose value at $k$ is written $v_{k}$ . Le…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T19:51:34.841888Z
Properties of the Absolute Value in an Ordered Field
lemmalem:absolute-value-properties-2026bAnalysis Algebra
Let $F$ be an ordered field and let $x,y,c\in F$ . Absolute values are as in that definition; $x-y$ abbreviates $x+(-y)$ and $x^{2}$ abbreviates $x\cdot x$ . For $s,t\in F$ we write $s<t$ to mean that $s\le t$ and $s\ne t$ . Then the following hold. 1. (Nonnegativity) $|x|$ equals…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T19:49:48.339666Z
Absolute Value in an Ordered Field
definitiondef:absolute-value-ordered-field-2026aAnalysis Algebra
Let $F$ be an ordered field, with order relation $\le$ , zero element $0$ , and additive inverse $-x$ of an element $x$ , and let $x\in F$ . The absolute value of $x$ is the element $|x|$ of $F$ given by…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T19:49:32.009361Z

Showing 21-40 of 76

Back Next

The Sum of nnn Ones is Strictly Increasing in nnn

Tuples in a Set

Dropping a Redundant Vector from a Spanning Family

Extraction of a Summand from a Finite Sum of Vectors

A Linear Subspace is a Vector Space and Inherits an Inner Product

The Span of a Finite Family is the Smallest Subspace Containing It

Finite-Dimensional Vector Space

Span of a Finite Family of Vectors

Concatenation of Finite Sums

Operations on Linear Operators

Sums, Scalar Multiples, Composites and the Identity are Linear Operators

Linear Operator on a Vector Space

Standard Basis Vectors of the Complex Coordinate Space

Finite Basis of a Vector Space

Finite Family Spanning a Vector Space

Linearly Independent Finite Family

Properties of Finite Sums of Vectors

Finite Sum Notation in a Vector Space

Properties of the Absolute Value in an Ordered Field

Absolute Value in an Ordered Field

The Sum of $n$ Ones is Strictly Increasing in $n$