-
How to instantiate a typeclass?
Take
Continue readingCoeOutas an example :
Recent Comments
How to instantiate a typeclass?
Take CoeOut as an example :
Equality Problem Find the equivalence of equality problem :
Continue readingNotes on the basic language, strategies, and recurring patterns used in proofs.
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.
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.
When talk about homomorphism, a few properties need to be considered, such as:
Continue readingDefinition 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 readingEquality Problem Find the equivalence of equality problem :
Continue reading