Skip to content

Decide what we mean by "irreducible ring element" and define it in the manual (possible in the is_irreducible docstring) #2328

@fingolfin

Description

@fingolfin

Notice while working on PR #1952: we don't actually define what we mean by "irreducible element" in a ring. Now for a integral domain, there is a no debate, the well-known definition works:

$a\in R$ is irreducible iff $\forall b,c\in R: a=bc$ implies $b$ is a unit or $c$ is a unit.

But what about commutative rings with zero divisors? Wikipedia discussed several incompatible definitions for this case. The "usual" above is apparently also called "very strongly irreducible" in this context, while they quote a source that suggests irreducible should mean "whenever $a=bc$ then $(a)=(b)$ or $(a)=(c)$".

One perfectly reasonable answer to this of course would be to just say we only define and support is_irreducible, factor, etc. over domains "in general" (specific implementations of non-domains then are of course still free to support these functions, they then just need to specify which notion of "irreducible" they have in mind).

If were to pick a definition, we should be careful to pick one that we can actually compute, and that actually is of interest to anyone. In other words: If we don't have a concrete application, it is probably best to just restrict this to domains, so that we can revisit this in the future if we have an application.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions