Theorems · Theorem · group theory
Set.image_mul_left
∀ {α : Type u_2} [inst : Group α] {t : Set α} {a : α}, (fun x => a * x) '' t = (fun x => a⁻¹ * x) ⁻¹' t- Cited by
- 21 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Groupstatement and proof · cited by 6,238
- Set.imagestatement · cited by 5,609
- Set.preimagestatement and proof · cited by 4,946
- inv_mul_cancel_leftproof · cited by 88
- mul_inv_cancel_leftproof · cited by 86
- Set.image_eq_preimage_of_inverseproof · cited by 27
Cited by21
Results whose statement or proof uses this declaration.
- singleton_mul_ballproof · cited by 3
- Set.image_mul_left'proof · cited by 2
- Subgroup.set_mul_normalizer_commproof · cited by 2
- Set.image_const_div_Iioproof · cited by 1
- Set.image_const_div_Ioiproof · cited by 1
- Finset.image_mul_leftproof · cited by 1
- closure_subset_mul_right_of_mem_nhds_one_of_invproof · cited by 1
- Subgroup.singleton_mul_subgroupproof · cited by 1
- Set.image_const_div_Icoproof · cited by 0
- Set.image_const_div_Iicproof · cited by 0
- Set.image_const_div_Iocproof · cited by 0
- Set.image_const_div_Iooproof · cited by 0