Kourovka 1.6

### What is the conjecture
The question "Is the group ring of a right-ordered group embeddable into a skew field?" (Problem 1.6 in the **Kourovka Notebook**, attributed to **A. I. Mal'cev**) is discussed in research papers, but it remains generally **open**.

While the answer is known to be **positive** for certain subclasses of groups, a complete solution (either a proof for all right-ordered groups or a counterexample) has not yet been found.

### Key Details and Research Status:
* **Origin:** The problem was posed by A. I. Mal'cev in the first edition of the Kourovka Notebook (1965). It asks whether the group ring $kG$ (where $k$ is a skew field and $G$ is a right-ordered group) can always be embedded into a division ring (skew field).
* **Solved Cases (Positive):**
* **Bi-ordered Groups:** Mal'cev himself (and independently B. H. Neumann) proved that if $G$ is **bi-ordered** (also called linearly ordered or simply ordered, meaning the order is invariant under multiplication on both sides), then the group ring $kG$ is embeddable into the **Mal'cev–Neumann series ring**, which is a division ring.
* **Locally Indicable Groups:** The result holds for locally indicable groups, a class that includes all bi-ordered groups.
* **Right-Ordered Case (The Open Problem):** Right-ordered groups form a strictly larger class than bi-ordered groups (e.g., the braid groups are right-orderable but not bi-orderable). For this broader class, the Mal'cev-Neumann construction does not directly apply.
* **N. I. Dubrovin** has made significant progress. In papers such as *"Rational closures of group rings of left-ordered groups"* (1994), he constructed embeddings for specific examples of right-ordered groups (like the universal cover of $SL(2, \mathbb{R})$) into skew fields. However, these constructions often result in division rings with "exotic" properties (e.g., containing prime ideals that are not completely prime), and his work did not resolve the problem for *every* right-ordered group.
* **Zero Divisors:** Since every right-ordered group is torsion-free, this problem is closely related to **Kaplansky's zero divisor conjecture**. If a counterexample to the zero divisor conjecture were found among right-ordered groups, it would immediately answer Mal'cev's question in the negative (since a ring with zero divisors cannot be embedded in a skew field). However, the zero divisor conjecture also remains open for this class.

**Conclusion:**
The question is actively discussed in the literature (e.g., by **N. I. Dubrovin**, **G. M. Bergman**, and others), but it is currently **unsolved**. It appears as an open problem in the most recent editions of the Kourovka Notebook.

**Reference:**
* *Unsolved Problems in Group Theory. The Kourovka Notebook.* (Various editions, e.g., 20th edition, 2022). Problem 1.6.

### Prerequisites needed

NOTE: the following is by Gemini, so double-check.

To state Mal’cev's question in Lean 4 (Mathlib), the primary **missing definition** is a bundled structure or typeclass for a **Right-Ordered Group**.

While Mathlib contains all the necessary building blocks (groups, linear orders, division rings, and group rings), it does not have a specific class named `RightOrderedGroup`. The existing `LinearOrderedGroup` class in Mathlib typically implies **bi-invariance** (the order is preserved under multiplication on both the left and the right), whereas a right-ordered group requires invariance only on the right.

### Missing Definition: `RightOrderedGroup`

To state the question, you would need to define a right-ordered group manually using mixins. A right-ordered group is a group $G$ with a linear order such that for all $a, b, c \in G$, if $a \le b$ then $ac \le bc$.

In Lean 4 Mathlib terms, this is expressed by combining:
* `[Group G]`
* `[LinearOrder G]`
* `[CovariantClass G G (Function.swap (*)) (· ≤ ·)]`

This third line asserts that the operation `(fun x y => y * x)` (which is right multiplication) is covariant with respect to the relation `≤`.

### Existing Definitions (Not Missing)

The other components of the question are already available in Mathlib:
* **Skew Field:** Available as `DivisionRing`. In Mathlib, a `DivisionRing` is an associative ring where every non-zero element has an inverse (synonymous with skew field).
* **Group Ring:** Available as `MonoidAlgebra`. The group ring $k[G]$ is expressed as `MonoidAlgebra k G`.
* **Embeddability:** Expressed via `RingHom` and `Function.Injective`.
* **The Question:** "Is the group ring of a right-ordered group embeddable into a skew field?" usually implies the coefficient ring is the integers $\mathbb{Z}$ or a field $k$. Both can be stated using `MonoidAlgebra`.

### Example Statement in Lean 4

Although the explicit `RightOrderedGroup` class is missing, you can state the problem using the existing components as follows:

```lean
import Mathlib.Algebra.MonoidAlgebra.Basic
import Mathlib.Algebra.Order.Group.Defs
import Mathlib.Algebra.Field.Defs

/--
Mal'cev's Question (Kourovka 1.6):
Is the group ring of a right-ordered group embeddable into a skew field?
-/
def MalcevQuestion : Prop :=
∀ (G : Type*) [Group G] [LinearOrder G]
-- The following line defines the "Right-Ordered" property:
-- Right multiplication preserves the order.
[CovariantClass G G (Function.swap (· * ·)) (· ≤ ·)],
∀ (k : Type*) [DivisionRing k], -- Coefficients from a Skew Field (or typically a Field)
∃ (D : Type*) [DivisionRing D], -- There exists a target Skew Field D
∃ (f : MonoidAlgebra k G →+* D), -- There exists a ring homomorphism f
Function.Injective f -- f is an embedding
```
### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-16

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else