Theorems · Theorem · group theory
sub_right_comm
∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b - c = a - c - b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext
- Assumes
- SubtractionCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- add_commproof · cited by 1,535
- sub_eq_add_negproof · cited by 1,023
- add_assocproof · cited by 746
- SubtractionCommMonoidstatement and proof · cited by 79
- add_left_commproof · cited by 76
Cited by15
Results whose statement or proof uses this declaration.
- toIcoDiv_sub_eq_toIcoDiv_addproof · cited by 3
- Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smulproof · cited by 3
- toIocDiv_sub_eq_toIocDiv_addproof · cited by 3
- toIcoMod_sub_eq_subproof · cited by 2
- Polynomial.isNilpotent_iterate_newtonMap_sub_of_isNilpotentproof · cited by 2
- toIocMod_sub_eq_subproof · cited by 2
- toIcoDiv_eq_floorproof · cited by 2
- cauchy_productproof · cited by 1
- AddCommGroup.modEq_nsmul_casesproof · cited by 1
- IsAdjoinRootMonic.map_modByMonicproof · cited by 1
- GenContFract.IntFractPair.exists_nth_stream_eq_none_of_ratproof · cited by 1
- WeakFEPair.f_modif_aux2proof · cited by 1