Density

Statistics

Metric	Count
Definitions	0
Theorems `dens_inv`, `dens_neg`, `dens_smul_finset`, `dens_vadd_finset`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`dens_inv` 📖	mathematical	—	`dens` `Finset` `inv` `InvolutiveInv.toInv`	—	`card_inv`
`dens_neg` 📖	mathematical	—	`dens` `Finset` `neg` `InvolutiveNeg.toNeg`	—	`card_neg`
`dens_smul_finset` 📖	mathematical	—	`dens` `Finset` `smulFinset` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`card_smul_finset`
`dens_vadd_finset` 📖	mathematical	—	`dens` `HVAdd.hVAdd` `Finset` `instHVAdd` `vaddFinset` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`card_vadd_finset`

---