Study of a division-like property

TL;DR

This paper introduces and explores a new division-like property called fadelian in noncommutative rings, providing theoretical results, examples, and formal proofs in Lean.

Contribution

It defines the fadelian property, proves its properties, constructs diverse examples, and formalizes results in Lean, expanding understanding of noncommutative ring structures.

Findings

Fadelian rings are not necessarily division rings.

Examples include non-Noetherian and non-Ore fadelian rings.

Formal proofs of properties are developed in Lean.

Abstract

We introduce a weak division-like property for noncommutative rings: a nontrivial ring is fadelian if for all nonzero $a,x$ there exist $b,c$ such that $x=ab+ca$. We prove properties of fadelian rings, and construct examples of such rings which are not division rings, as well as non-Noetherian and non-Ore examples. We have also formalized some of these results in the Lean proof assistant.