Theorems · Theorem · group theory
AddSemiconjBy.eq
∀ {S : Type u_1} [inst : Add S] {a x y : S}, AddSemiconjBy a x y → a + x = y + aEquality behind AddSemiconjBy a x y; useful for rewriting.
- Defined in
- Mathlib.Algebra.Group.Semiconj.Defs
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- Add
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddSemiconjBystatement and proof · cited by 56
Cited by10
Results whose statement or proof uses this declaration.
- AddSemiconjBy.addUnits_neg_rightproof · cited by 3
- AddSemiconjBy.addUnits_neg_symm_leftproof · cited by 3
- AddSemiconjBy.add_leftproof · cited by 3
- AddSemiconjBy.vadd_leftproof · cited by 2
- AddSemiconjBy.vadd_rightproof · cited by 2
- AddSemiconjBy.add_rightproof · cited by 2
- AddSemiconjBy.eq_zero_iffproof · cited by 1
- AddSemiconjBy.function_semiconj_add_leftproof · cited by 1
- AddSemiconjBy.function_semiconj_add_right_swapproof · cited by 1
- AddMonoidHom.map_isAddConjproof · cited by 0