Theorems · Theorem · group theory
neg_vadd_eq_iff
∀ {G : Type u_3} {α : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a b : α}, -g +ᵥ a = b ↔ a = g +ᵥ b- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
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.
- AddGroupstatement and proof · cited by 4,410
- HVAdd.hVAddstatement and proof · cited by 1,820
- AddActionstatement and proof · cited by 820
- neg_vadd_vaddproof · cited by 34
- vadd_neg_vaddproof · cited by 31
Cited by13
Results whose statement or proof uses this declaration.
- Set.mem_neg_vadd_set_iffproof · cited by 5
- AddAction.isBlock_iff_disjoint_vadd_of_neproof · cited by 3
- AddAction.fixedBy_negproof · cited by 3
- SubAddAction.ofStabilizer.isMultiplyPretransitiveproof · cited by 2
- AddAction.zsmul_vadd_eq_iff_period_dvdproof · cited by 2
- SubAddAction.addConjMap_ofFixingAddSubgroup_bijectiveproof · cited by 1
- IsAddQuotientCoveringMap.isCancelVAddproof · cited by 1
- Set.addConj_mem_fixingAddSubgroupproof · cited by 1
- faithfulVAdd_iffproof · cited by 1
- SubAddAction.fixingAddSubgroup_map_addConj_eqproof · cited by 1
- AddAction.IsBlock.of_orbitproof · cited by 0
- vadd_mem_fixedPoints_of_normalproof · cited by 0