Structures · Algebra
OreLocalization.OreSet
A submonoid S of a monoid R is (left) Ore if common factors on the right can be turned
into common factors on the left, and if each pair of r : R and s : S admits an Ore numerator
v : R and an Ore denominator u : S such that u * r = v * s.
- Shape
- One type argument · adds ore_right_cancel, oreNum, oreDenom, ore_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by152
- OreLocalization
- OreLocalization.oreDiv
- OreLocalization.ind
- OreLocalization.oreNum
- OreLocalization.oreDenom
- OreLocalization.one_def
- OreLocalization.oreDiv_eq_iff
- OreLocalization.oreDiv_smul_char
- OreLocalization.zero_oreDiv
- OreLocalization.oreDiv_mul_char
- OreLocalization.numeratorHom
- OreLocalization.zero_def
- OreLocalization.expand
- OreLocalization.add_oreDiv
- OreLocalization.universalMulHom
- OreLocalization.oreDivAddChar'
- OreLocalization.universalHom
- OreLocalization.smul_oreDiv
- OreLocalization.neg_def
- OreLocalization.expand'
- OreLocalization.zero_oreDiv'
- OreLocalization.oreDiv_smul_oreDiv
- OreLocalization.smul_one_oreDiv_one_smul
- OreLocalization.numeratorHom_apply
- OreLocalization.oreDiv_one_surjective_of_finite_right
- OreLocalization.oreDiv_one_surjective_of_finite_left
- OreLocalization.oreDiv_add_oreDiv
- OreLocalization.oreDiv_add_char'
- OreLocalization.oreDivSMulChar'
- OreLocalization.oreEqv
- OreLocalization.ore_eq
- OreLocalization.nontrivial_iff
- OreLocalization.cardinalMk_le
- OreLocalization.inv_def
- OreLocalization.smul_div_one
- OreLocalization.oreDiv_add_char
- OreLocalization.oreCondition
- OreLocalization.numeratorRingHom
- OreLocalization.oreDiv_mul_oreDiv
- OreLocalization.div_eq_one
- OreLocalization.OreSet.oreNum
- OreLocalization.smul_cancel'
- OreLocalization.nontrivial_of_nonZeroDivisorsLeft
- OreLocalization.mul_inv
- OreLocalization.mul_cancel
- OreLocalization.numeratorHom_inj
- OreLocalization.div_eq_one'
- OreLocalization.universalMulHom_apply
- OreLocalization.add_smul
- OreLocalization.OreSet.ore_right_cancel
Ancestors0
No ancestors.