Cardinality of sets under pointwise group with zero operations

theorem Cardinal.mk_smul_set₀ {G₀ : Type u_1} {M₀ : Type u_2} [GroupWithZero G₀] [Zero M₀] [MulActionWithZero G₀ M₀] {a : G₀} (ha : a ≠ 0) (s : Set M₀) : mk ↑(a • s) = mk ↑s

theorem Set.natCard_smul_set₀ {G₀ : Type u_1} {M₀ : Type u_2} [GroupWithZero G₀] [Zero M₀] [MulActionWithZero G₀ M₀] {a : G₀} (ha : a ≠ 0) (s : Set M₀) : Nat.card ↑(a • s) = Nat.card ↑s