PointwisePi

Statistics

Metric	Count
Definitions	0
Theorems `smul_pi`, `smul_pi_subset`, `smul_pi₀`, `smul_univ_pi`, `vadd_pi`, `vadd_pi_subset`, `vadd_univ_pi`	7
Total	7

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_pi` 📖	mathematical	—	`Set` `Set.smulSet` `Pi.instSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.pi`	—	`Set.piMap_image_pi` `MulAction.surjective`
`smul_pi_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smulSet` `Pi.instSMul` `Set.pi`	—	`Set.piMap_image_pi_subset`
`smul_pi₀` 📖	mathematical	—	`Set` `Set.smulSet` `Pi.instSMul` `SemigroupAction.toSMul` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `MonoidWithZero.toMonoid` `Set.pi`	—	`smul_pi`
`smul_univ_pi` 📖	mathematical	—	`Set` `Set.smulSet` `Pi.instSMul` `Set.pi` `Set.univ`	—	`Set.piMap_image_univ_pi`
`vadd_pi` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `Pi.instVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.pi`	—	`Set.piMap_image_pi` `AddAction.surjective`
`vadd_pi_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `Pi.instVAdd` `Set.pi`	—	`Set.piMap_image_pi_subset`
`vadd_univ_pi` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `Pi.instVAdd` `Set.pi` `Set.univ`	—	`Set.piMap_image_univ_pi`

---