Étude d'une propriété semblable à la divisibilité

Abstract

Nous introduisons une propriété de division faible pour les anneaux non-commutatifs : un anneau non-trivial est fadélien si pour tout a, x non nuls il existe b, c tels que x=ab+ca. Nous prouvons des propriétés des anneaux fadeliens, et construisons des exemples de tels anneaux qui ne sont pas des anneaux à division, ainsi que des exemples non-noethériens et non-Ore. Certains de ces résultats sont formalisés à l'aide de l'assistant de preuve Lean.