Freedom Math Dance

That formula of Cayley asserts that there are $n^{n-2}$ trees with vertices labeled $1,\dots,n$. This is a chapter in graph theory, in which...

This post is here to record a fact that ought to be better known and for which I ought to have known a proper proof beforehand. Let's s...

In the previous post , I had explained how I could prove a general version of the classic fact that transvections have determinant 1. Recall...

A transvection in a $K$-vector space $V$ is a linear map $T(f,v)$ of the form $x\mapsto x + f(x) v$, where $f\in V^*$ is a linear form and ...

Sometimes in mathematics, you are told about very elementary things of which you hadn't even thought. I was well aware of some “duality”...

Let $R$ be a ring. Its Krull dimension is the supremum of the lengths $n$ of chains $P_0\subsetneq P_1 \subsetneq\dots\subsetneq P_n$ of pri...

I've been formalizing mathematical theorems in Lean for some years now, and one of the major blocks is the difficulty of formalizing ele...