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