Order_of_Subset_Product_with_Singleton_v5
Provedcardinalitygroup-theoryproofwikisubset-product
Let G be a group. Multiplying a set Y on the left by a single element x preserves cardinality: |xY| = |Y|.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Subset_Product_with_Singleton_v5 {G : Type _} [Group G] (x : G) (Y : Set G) : Set.ncard ((fun y => x * y) '' Y) = Set.ncard Y := by sorrySource