Card

📁 Source: Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean

Statistics

Metric	Count
Definitions	0
Theorems mk_smul_set₀, natCard_smul_set₀	2
Total	2

Cardinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_smul_set₀ 📖	mathematical	—	Set.Elem Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero MulActionWithZero.toSMulWithZero	—	mk_image_eq_of_injOn Function.Injective.injOn MulAction.injective₀

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCard_smul_set₀ 📖	mathematical	—	Nat.card Elem Set smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero MulActionWithZero.toSMulWithZero	—	Nat.card_image_of_injective MulAction.injective₀

---

← Back to Index