Theorems · Theorem · group theory
QuotientAddGroup.preimage_image_mk
∀ {α : Type u_1} [inst : AddGroup α] (N : AddSubgroup α) (s : Set α),
QuotientAddGroup.mk ⁻¹' QuotientAddGroup.mk '' s = ⋃ x, (fun x_1 => x_1 + ↑x) ⁻¹' s- Defined in
- Mathlib.GroupTheory.Coset.Defs
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 70 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.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.imagestatement · cited by 5,609
- Set.preimagestatement · cited by 4,946
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement and proof · cited by 3,232
- Set.iUnionstatement · cited by 2,483
- HasQuotient.Quotientstatement · cited by 2,301
- Set.extproof · cited by 2,266
- neg_negproof · cited by 960
- QuotientAddGroup.mkstatement and proof · cited by 348
- neg_add_revproof · cited by 236
- Set.mem_iUnionproof · cited by 212
Cited by2
Results whose statement or proof uses this declaration.
- QuotientAddGroup.preimage_image_mk_eq_iUnion_imageproof · cited by 1
- AddSubgroup.card_add_eq_card_addSubgroup_add_card_quotientproof · cited by 0