Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Every Euclidean linear map has a unique matrix and satisfies for some
Statement
For every linear there is a unique matrix such that . Moreover there is with for every .
Facts & Assumptions
Given: A Euclidean linear map .
The coordinate list of with respect to the ordered basis is its ordinary coordinate list, and (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ).
The Euclidean norm of is , and it is a norm (The Euclidean inner product on ).
Proof
Put . By [L1] and linearity, , so .
The columns determine every value in step 1.1, and evaluating the displayed formula at shows that every representing matrix has exactly these entries; thus the matrix is unique.
Let . Cauchy--Schwarz [L3] in each row and summing gives , hence .
Depends on
- A linear map $L:\mathbb{R}^m\to\mathbb{R}^n$ in Euclidean coordinates
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$, the parallelogram law and polarisation
Used by
- Lebesgue measure on ℝⁿ is invariant under every orthogonal linear map Corollary
- The Jordan content of the parallelepiped spanned by the columns of a square real matrix is the absolute value of its determinant Corollary
- The exponential map of a flat torus is not injective Example
- A coordinate scaling and a coordinate transposition send the unit cube to a set of measure equal to the absolute value of the determinant Lemma
- A shear sends the unit cube to a set of Lebesgue measure one Lemma
- Newton maps are uniform contractions near a point with invertible derivative Lemma
- Smooth orientation sign is the local integral homology multiplier Lemma
- A holomorphic function of several variables is continuous and separately holomorphic Proposition
- Sums, products and nonvanishing quotients of holomorphic functions are holomorphic Proposition
- A conjugate difference quotient characterizes antiholomorphic maps Theorem
- A linear endomorphism of ℝⁿ sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant Theorem
- A linear map T of ℝⁿ sends Lebesgue measurable sets to Lebesgue measurable sets, with λₙ(T[E])=|det T| λₙ(E) when T is invertible and T[E] Lebesgue null when it is not Theorem
- A total derivative computes every directional derivative, and its matrix is the Jacobian Theorem
- An invertible linear map of ℝⁿ scales the Lebesgue measure of every Borel set by a positive constant depending only on the map Theorem
- Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with ∂_z̄f=0, or with the Cauchy–Riemann equations Theorem
- Every affine hyperplane of ℝⁿ, and hence every proper linear subspace, is Lebesgue null Theorem
- The chain rule for total derivatives: D(g∘ f)(a)=Dg(f(a))∘ Df(a) Theorem
- The composite of holomorphic maps is holomorphic and its complex Jacobian is the product Theorem
- The Euclidean implicit function theorem with derivative formula Theorem
- Total differentiability gives a local O(‖h‖₂) increment bound and therefore continuity Theorem
Dependency tree · two levels
52 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- J. Lebl, Basic Analysis I, §8.3 (standard reference, not scraped)