Theorems · Theorem · group theory
QuotientAddGroup.rightRel_apply
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, (QuotientAddGroup.rightRel s) x y ↔ y + -x ∈ s- Defined in
- Mathlib.GroupTheory.Coset.Defs
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- AddSubgroupstatement and proof · cited by 3,232
- eq_neg_add_iff_add_eqproof · cited by 16
- QuotientAddGroup.rightRelstatement · cited by 14
- add_neg_eq_iff_eq_addproof · cited by 12
- exists_neg_mem_iff_exists_memproof · cited by 3
Cited by6
Results whose statement or proof uses this declaration.
- AddSubgroup.IsComplement.add_neg_toRightFun_memproof · cited by 6
- Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroupproof · cited by 3
- AddSubgroup.isComplement_addSubgroup_left_iff_existsUnique_quotientMk''proof · cited by 1
- QuotientAddGroup.rightRel_eqproof · cited by 0
- QuotientAddGroup.rightRel_piproof · cited by 0
- QuotientAddGroup.rightRel_prodproof · cited by 0