Freedom Math Dance

In its classical statement, the theorem of Gelfand-Mazur is the following: Theorem 1. — Let $K$ be a complete normed field which is an extension of the field $\mathbf C$ of complex numbers.

That formula of Cayley asserts that there are $n^{n-2}$ trees with vertices labeled $1,\dots,n$.

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.

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

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 $v\in V$ is a vector such that $f(v)=0$.

Sometimes in mathematics, you are told about very elementary things of which you hadn't even thought.

Let $R$ be a ring.

I've been formalizing mathematical theorems in Lean for some years now, and one of the major blocks is the difficulty of formalizing elementary results that mathematicians do not take the time to even state.

Browsing through my Zotero database, I fall upon a paper by Harald Kuhn where he proposes an elementary proof of the Weierstrass approximation theorem.

This is an exposition of the proof of the inequality between arithmetic and geometric means given by A.

Recently, in the Zulip server for Lean users, somebody went with something that looked like homework, but managed to sting me a little bit.

Kronecker's theorem of the title is the following.

Reading a book on philosophy of mathematics, even if it's written lightly, such as that one, Why is there philosophy of mathematics at all?

The “combinatorial Nullstellensatz” is a relatively elementary statement due to Noga Alon (1999) whose name, while possibly frightening, really says what it is and what it is good for.

Divided powers are an algebraic gadget that emulate, in an arbitrary ring, the functions $x\mapsto x^n/n!

$\gdef\abs#1{\lvert#1\rvert}$ There are many parts of number theory I don't know of, and today's story is about one I learnt very recently, at the intersection of number theory and computer science.

Let $E$ and $F$ be normed vector spaces, over the real or complex numbers, and let $u\colon E\to F$ be a linear map.

Polynomials are an algebraic gadget, and one is rarely led to think about the topology a ring of polynomials should carry.

Projective modules and flat modules are two important concepts in algebra, because they characterize those modules for which a general functorial construction (Hom module and tensor product, respectively) behave better than what is the case for general mo…

$\global\def\Card{\operatorname{Card}}\global\def\GL{\mathrm{GL}}\global\def\im{\operatorname{im}}\gdef\KVar{\mathrm{KVar}}$ Let $n$ be an integer and $F$ be a field.

Let $T_1,\dots,T_n$ be indeterminates.

This is a swift adaptation of a thread on Mastodon written after having read the beginning of Mara Goyet's column in yesterday's edition of Le Monde (please don't spoil the game by jumping to it now).

I would like to tell here a story that runs over some 150 years of mathematics, around the following question: given a power series $\sum a_n T^n$ (in one variable), how can you tell it comes from a rational function?

$\gdef\ann{\mathop{\mathrm{ann}}} \gdef\Ass{\mathop{\mathrm{Ass}}}\gdef\Spec{\mathop{\mathrm{Spec}}}$ I would like to go back to a quite delicate question of commutative algebra, that of associated prime ideals of modules.

The following reflexion came out of my irrepressible need to understand why the 3 double transpositions in $\mathfrak S_4$, together with the identity, formed a group $V$.