Practical_tips

  1. How to instantiate a typeclass?

    Take CoeOut as an example :

    Continue reading →
Posted in Formal Verification | Leave a comment

Summary

Fundamentals

Basic Logic Inference

  1. $P \to Q, P \implies Q$
  2. $P \to Q, \neg Q \implies \neg P$
  3. $P \lor Q, \neg P \implies Q$
  4. $P (\text{or } Q) \implies P \lor Q$
  5. $P, Q \implies P \land Q$
  6. $P \land Q \implies P (\text{or } Q)$
  7. $P \lor Q \to R \implies (P \to R) \land (Q \to R)$

Equivalence

Equality Problem Find the equivalence of equality problem :

Continue reading →
Posted in Math of Proof | Leave a comment

Index

Notes on the basic language, strategies, and recurring patterns used in proofs.

Parts

Continue reading →
Posted in Math of Proof | Leave a comment

Index

Parts

Posted in Linear Algebra | Leave a comment

Ring

Table of Contents

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*} [CommRing A]; later snippets may use earlier declarations.

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) which is performed on vectors in the domain, resulting in vectors in the codomain.

Homomorphism

When talk about homomorphism, a few properties need to be considered, such as:

Continue reading →
Posted in Linear Algebra | Leave a comment

Ch05 Ch09

Table of Contents

Table of Contents

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 invariant subspace under $T$. We call $T|_U$ is an operator on $U$.

Continue reading →
Posted in Linear Algebra | Leave a comment

Index

Notes on mathematical concepts, proofs, and examples.

Topics

Posted in Mathematics | Leave a comment

Ch04 Ch06

Table of Contents

Table of Contents

Eigenvalues and Eigenvectors

Inner Product Spaces

Posted in Linear Algebra | Leave a comment

Part 1

Fundamentals

Basic Logic Inference

  1. $P \to Q, P \implies Q$
  2. $P \to Q, \neg Q \implies \neg P$
  3. $P \lor Q, \neg P \implies Q$
  4. $P (\text{or } Q) \implies P \lor Q$
  5. $P, Q \implies P \land Q$
  6. $P \land Q \implies P (\text{or } Q)$
  7. $P \lor Q \to R \implies (P \to R) \land (Q \to R)$

Equivalence

Equality Problem Find the equivalence of equality problem :

Continue reading →
Posted in Math of Proof | Leave a comment