Theorems · Theorem · group theory
Algebra.GrothendieckAddGroup.mk_sub_mk
∀ {M : Type u_1} [inst : AddCommMonoid M] (m₁ m₂ : M) (s₁ s₂ : ↥⊤),
AddLocalization.mk m₁ s₁ - AddLocalization.mk m₂ s₂ = AddLocalization.mk (m₁ + ↑s₂) ⟨↑s₁ + m₂, ⋯⟩- Cited by
- 0 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement and proof · cited by 12,281
- Top.topstatement and proof · cited by 9,680
- AddSubmonoidstatement · cited by 1,178
- sub_eq_add_negproof · cited by 1,023
- AddLocalizationstatement · cited by 38
- AddLocalization.mkstatement and proof · cited by 28
- AddSubmonoid.mem_topstatement and proof · cited by 20
- AddLocalization.mk_addproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.