HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k stars 185 forks source link

Idempotent ring elements #2009

Open Alizter opened 4 days ago

Alizter commented 4 days ago

We should define what it means for a ring element to be idempotent and prove some basic properties about them.

We should also link this to decomposition of $R$-modules. if $e$ is an idempotent element of $R$ then an $R$-module $M$ can be decomposed as $M \cong eM \oplus (1-e)M$. This will be important for an eventual proof of the Wedderburn-Artin theorem.