Theorems · Inductive type · ring theory
AddOreLocalization.AddOreSet
{R : Type u_1} → [inst : AddMonoid R] → AddSubmonoid R → Type u_1A submonoid S of an additive monoid R is (left) Ore if common summands on the right can be
turned into common summands on the left, and if each pair of r : R and s : S admits an Ore
minuend v : R and an Ore subtrahend u : S such that u + r = v + s.
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement · cited by 2,864
- AddSubmonoidstatement · cited by 1,178
Cited by75
Results whose statement or proof uses this declaration.
- AddOreLocalizationstatement and proof · cited by 44
- AddOreLocalization.oreSubstatement and proof · cited by 40
- AddOreLocalization.oreSub_add_charstatement and proof · cited by 8
- AddOreLocalization.indstatement and proof · cited by 8
- AddOreLocalization.oreSubtrastatement and proof · cited by 7
- AddOreLocalization.oreMinstatement and proof · cited by 7
- AddOreLocalization.oreSub_vadd_charstatement and proof · cited by 6
- AddOreLocalization.oreSub_eq_iffstatement and proof · cited by 5
- AddOreLocalization.zero_defstatement and proof · cited by 5
- AddOreLocalization.numeratorHomstatement and proof · cited by 5
- AddOreLocalization.universalAddHomstatement and proof · cited by 3
- AddOreLocalization.oreSub_zero_surjective_of_finite_leftstatement and proof · cited by 2