Monday, December 12, 2022

Multiplicative square roots

›
I will just discuss briefly the first section of a paper by William Waterhouse (2012), “ Square Root as a Homomorphism ” ( American Mat...
Tuesday, November 1, 2022

#Mathober2022

›
Sophia Wood (@fractalkitty) had the good idea to set up a #Mathober project: for each day of october, she proposes you to react to one word ...
Tuesday, September 13, 2022

Yet another post on simplicity

›
I see that I finally arrive to an end of my journey in formalizing in Lean the simplicity of the alternating group in 5 letters or more, so ...
1 comment :
Tuesday, December 21, 2021

The very simple proof that the alternating group on 5 letters (or more) is simple

›
\( \def\supp {\operatorname{supp}} \) As explained in the previous post, I wanted to formalize the proof that the alternating group on 5 let...
1 comment :
Monday, December 13, 2021

Not simple proofs of simplicity

›
The last few weeks, I started my self-education in proof formalization (in Lean) by a test case, the simplicity of the alternating group. In...
1 comment :
Thursday, April 22, 2021

Growth of the Gaussian pivoting algorithm

›
“ Gaussian elimination ” is the standard method for solving systems of linear equations that runs by choosing one pivot variable in one of ...
Friday, April 2, 2021

On the Hadamard-Lévy theorem, or is it Banach-Mazur?

›
During the preparation of an agrégation lecture on connectedness, I came across the following theorem, attributed to Hadamard–Lévy:  Theor...