Documentation Verification Report

Card

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

Statistics

Metric	Count
Definitions	0
Theorems `mk_add_le`, `mk_div_le`, `mk_inv`, `mk_mul_le`, `mk_neg`, `mk_smul_set`, `mk_sub_le`, `mk_vadd_set`, `encard_inv`, `encard_neg`, `encard_smul_set`, `encard_vadd_set`, `natCard_add_le`, `natCard_div_le`, `natCard_inv`, `natCard_mul_le`, `natCard_neg`, `natCard_smul_set`, `natCard_sub_le`, `natCard_vadd_set`, `ncard_inv`, `ncard_neg`, `ncard_smul_set`, `ncard_vadd_set`	24
Total	24

Cardinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_add_le` 📖	mathematical	—	`Cardinal` `instLE` `Set.Elem` `Set` `Set.add` `instMul`	—	`Set.image2_add` `mk_image2_le`
`mk_div_le` 📖	mathematical	—	`Cardinal` `instLE` `Set.Elem` `Set` `Set.div` `DivInvMonoid.toDiv` `instMul`	—	`Set.image2_div` `mk_image2_le`
`mk_inv` 📖	mathematical	—	`Set.Elem` `Set` `Set.inv` `InvolutiveInv.toInv`	—	`Set.image_inv_eq_inv` `mk_image_eq_of_injOn` `Function.Injective.injOn` `inv_injective`
`mk_mul_le` 📖	mathematical	—	`Cardinal` `instLE` `Set.Elem` `Set` `Set.mul` `instMul`	—	`Set.image2_mul` `mk_image2_le`
`mk_neg` 📖	mathematical	—	`Set.Elem` `Set` `Set.neg` `InvolutiveNeg.toNeg`	—	`Set.image_neg_eq_neg` `mk_image_eq_of_injOn` `Function.Injective.injOn` `neg_injective`
`mk_smul_set` 📖	mathematical	—	`Set.Elem` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`mk_image_eq_of_injOn` `Function.Injective.injOn` `MulAction.injective`
`mk_sub_le` 📖	mathematical	—	`Cardinal` `instLE` `Set.Elem` `Set` `Set.sub` `SubNegMonoid.toSub` `instMul`	—	`Set.image2_sub` `mk_image2_le`
`mk_vadd_set` 📖	mathematical	—	`Set.Elem` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`mk_image_eq_of_injOn` `Function.Injective.injOn` `AddAction.injective`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`encard_inv` 📖	mathematical	—	`encard` `Set` `inv` `InvolutiveInv.toInv`	—	`Cardinal.mk_inv`
`encard_neg` 📖	mathematical	—	`encard` `Set` `neg` `InvolutiveNeg.toNeg`	—	`Cardinal.mk_neg`
`encard_smul_set` 📖	mathematical	—	`encard` `Set` `smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Cardinal.mk_smul_set`
`encard_vadd_set` 📖	mathematical	—	`encard` `HVAdd.hVAdd` `Set` `instHVAdd` `vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Cardinal.mk_vadd_set`
`natCard_add_le` 📖	mathematical	—	`Nat.card` `Elem` `Set` `add`	—	`infinite_or_finite` `Infinite.card_eq_zero` `zero_le` `Nat.instCanonicallyOrderedAdd` `Cardinal.toNat_mul` `Cardinal.toNat_le_toNat` `Cardinal.mk_add_le` `Cardinal.mul_lt_aleph0_iff` `Cardinal.lt_aleph0_iff_subtype_finite` `finite_add` `IsCancelAdd.toIsLeftCancelAdd` `IsCancelAdd.toIsRightCancelAdd` `Cardinal.mk_eq_zero` `instIsEmptyElemEmptyCollection` `finite_empty`
`natCard_div_le` 📖	mathematical	—	`Nat.card` `Elem` `Set` `div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div_eq_mul_inv` `natCard_inv` `natCard_mul_le` `CancelMonoid.toIsCancelMul`
`natCard_inv` 📖	mathematical	—	`Nat.card` `Elem` `Set` `inv` `InvolutiveInv.toInv`	—	`ncard_inv`
`natCard_mul_le` 📖	mathematical	—	`Nat.card` `Elem` `Set` `mul`	—	`infinite_or_finite` `Infinite.card_eq_zero` `Nat.instCanonicallyOrderedAdd` `Cardinal.toNat_le_toNat` `Cardinal.mk_mul_le` `IsCancelMul.toIsLeftCancelMul` `IsCancelMul.toIsRightCancelMul` `Cardinal.mk_eq_zero` `instIsEmptyElemEmptyCollection`
`natCard_neg` 📖	mathematical	—	`Nat.card` `Elem` `Set` `neg` `InvolutiveNeg.toNeg`	—	`ncard_neg`
`natCard_smul_set` 📖	mathematical	—	`Nat.card` `Elem` `Set` `smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`ncard_smul_set`
`natCard_sub_le` 📖	mathematical	—	`Nat.card` `Elem` `Set` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `natCard_neg` `natCard_add_le` `AddCancelMonoid.toIsCancelAdd`
`natCard_vadd_set` 📖	mathematical	—	`Nat.card` `Elem` `HVAdd.hVAdd` `Set` `instHVAdd` `vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`ncard_vadd_set`
`ncard_inv` 📖	mathematical	—	`ncard` `Set` `inv` `InvolutiveInv.toInv`	—	`encard_inv`
`ncard_neg` 📖	mathematical	—	`ncard` `Set` `neg` `InvolutiveNeg.toNeg`	—	`encard_neg`
`ncard_smul_set` 📖	mathematical	—	`ncard` `Set` `smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`encard_smul_set`
`ncard_vadd_set` 📖	mathematical	—	`ncard` `HVAdd.hVAdd` `Set` `instHVAdd` `vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`encard_vadd_set`

---

← Back to Index