# (Right) Ore sets #

This defines right Ore sets on arbitrary monoids.

## References #

- https://ncatlab.org/nlab/show/Ore+set

A submonoid `S`

of a monoid `R`

is (right) Ore if common factors on the left can be turned
into common factors on the right, and if each pair of `r : R`

and `s : S`

admits an Ore numerator
`v : R`

and an Ore denominator `u : S`

such that `r * u = s * v`

.

Common factors on the left can be turned into common factors on the right, a weak form of cancellability.

- oreNum : R → ↥S → R
The Ore numerator of a fraction.

- oreDenom : R → ↥S → ↥S
The Ore denominator of a fraction.

- ore_eq : ∀ (r : R) (s : ↥S), r * ↑(OreLocalization.OreSet.oreDenom r s) = ↑s * OreLocalization.OreSet.oreNum r s

## Instances

Common factors on the left can be turned into common factors on the right, a weak form of cancellability.

The Ore numerator of a fraction.

## Equations

## Instances For

The Ore denominator of a fraction.

## Equations

## Instances For

The Ore condition of a fraction, expressed in terms of `oreNum`

and `oreDenom`

.

The Ore condition bundled in a sigma type. This is useful in situations where we want to obtain both witnesses and the condition for a given fraction.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The trivial submonoid is an Ore set.

## Equations

- One or more equations did not get rendered due to their size.

Every submonoid of a commutative monoid is an Ore set.

## Equations

- One or more equations did not get rendered due to their size.

Cancellability in monoids with zeros can act as a replacement for the `ore_left_cancel`

condition of an ore set.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

In rings without zero divisors, the first (cancellability) condition is always fulfilled, it suffices to give a proof for the Ore condition itself.

## Equations

- OreLocalization.oreSetOfNoZeroDivisors oreNum oreDenom ore_eq = OreLocalization.oreSetOfCancelMonoidWithZero oreNum oreDenom ore_eq