Recent Comments
Monthly Archives: September 2026
Structures
Invariant Subspaces Definition 5.1 – Invariant Subspace Let $T \in \mathcal{L}(V)$ be a (linear) operator on vector space $V$. When we restrict $T$ to a subspace $U \subseteq V$, we are not sure the corresponding vectors will still lie in $U$. If they do, we say that $U$ is an… Continue reading
Posted in Linear Algebra
Leave a comment
Practical_tips
How to instantiate a typeclass? Take CoeOut as an example : Continue reading
Posted in Formal Verification
Leave a comment
Summary
Fundamentals Basic Logic Inference $P \to Q, P \implies Q$ $P \to Q, \neg Q \implies \neg P$ $P \lor Q, \neg P \implies Q$ $P (\text{or } Q) \implies P \lor Q$ $P, Q \implies P \land Q$ $P \land Q \implies P (\text{or } Q)$ $P \lor Q… Continue reading
Posted in Math of Proof
Leave a comment
Index
Notes on the basic language, strategies, and recurring patterns used in proofs. Parts summary-math-of-proof Continue reading
Posted in Math of Proof
Leave a comment
Index
Parts Fundamentals Structures Summary Continue reading
Posted in Linear Algebra
Leave a comment
Ring
Note that all rings considered here are commutative and have a multiplicative identity. Each written proof or proof sketch is followed by a separate folded Lean 4 proof. The snippets are collected and compiled in mathlib-in-lean/commutative-algebra/Ring.lean . They assume that file’s imports, namespace CommAlg , and variable {A : Type*}… Continue reading
Posted in Commutative Algebra
Leave a comment
Summary
Linear map is a special type of homomorphism between vector spaces, which preserves the operations of vector addition and scalar multiplication : $$ T(\mathbf{u} + \mathbf{v}) = T(\mathbf{u}) + T(\mathbf{v}), \quad T(c\mathbf{v}) = c T(\mathbf{v}) $$ So we can also treat linear map as a kind of transformation (or action)… Continue reading
Posted in Linear Algebra
Leave a comment
Ch05 Ch09
Invariant Subspaces Definition 5.1 – Invariant Subspace Let $T \in \mathcal{L}(V)$ be a (linear) operator on vector space $V$. When we restrict $T$ to a subspace $U \subseteq V$, we are not sure the corresponding vectors will still lie in $U$. If they do, we say that $U$ is an… Continue reading
Posted in Linear Algebra
Leave a comment
Index
Notes on mathematical concepts, proofs, and examples. Topics Linear Algebra Continue reading
Posted in Mathematics
Leave a comment
Ch04 Ch06
Table of Contents Table of Contents Polynomials Eigenvalues and Eigenvectors Inner Product Spaces Eigenvalues and Eigenvectors Inner Product Spaces
Posted in Linear Algebra
Leave a comment