Cardinality of sets under pointwise group with zero operations #
theorem
Cardinal.mk_smul_set₀
{G₀ : Type u_2}
{M₀ : Type u_4}
[GroupWithZero G₀]
[Zero M₀]
[MulActionWithZero G₀ M₀]
{a : G₀}
(ha : a ≠ 0)
(s : Set M₀)
:
Cardinal.mk ↑(a • s) = Cardinal.mk ↑s
theorem
Set.natCard_smul_set₀
{G₀ : Type u_2}
{M₀ : Type u_4}
[GroupWithZero G₀]
[Zero M₀]
[MulActionWithZero G₀ M₀]
{a : G₀}
(ha : a ≠ 0)
(s : Set M₀)
: