Theorems · Definition · ring theory
AddOreLocalization.oreMin
{R : Type u_1} → [inst : AddMonoid R] → {S : AddSubmonoid R} → [AddOreLocalization.AddOreSet S] → R → ↥S → RThe Ore minuend of a difference.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement and proof · cited by 2,864
- AddSubmonoidstatement and proof · cited by 1,178
- AddOreLocalization.AddOreSetstatement and proof · cited by 50
- AddOreLocalization.AddOreSet.oreMinproof · cited by 1
Cited by11
Results whose statement or proof uses this declaration.
- AddOreLocalization.addOreConditionproof · cited by 2
- AddOreLocalization.vadd_oreSubstatement · cited by 2
- AddOreLocalization.oreSubAddChar'proof · cited by 1
- AddOreLocalization.oreSubVAddChar'proof · cited by 1
- AddOreLocalization.oreSub_add_oreSubstatement · cited by 1
- AddOreLocalization.oreSub_vadd_oreSubstatement · cited by 1
- AddOreLocalization.oreSub_zero_vaddproof · cited by 1
- AddOreLocalization.vadd_zero_vaddproof · cited by 1
- AddOreLocalization.hvaddproof · cited by 0
- AddOreLocalization.addOreSetComm_oreMinstatement · cited by 0
- AddOreLocalization.add_ore_eqstatement · cited by 0