Pointwise

Statistics

Metric	Count
Definitions	0
Theorems `const_smul`, `const_smul_of_ne_zero`, `const_smul₀`, `const_vadd`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	mathematical	`MeasurableSet`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Set.preimage_smul_inv` `MeasurableConstSMul.measurable_const_smul`
`const_smul_of_ne_zero` 📖	mathematical	`MeasurableSet`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`Set.preimage_smul_inv₀` `MeasurableConstSMul.measurable_const_smul`
`const_smul₀` 📖	mathematical	`MeasurableSet`	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `MulActionWithZero.toSMulWithZero`	—	`eq_or_ne` `Set.Subsingleton.measurableSet` `Set.subsingleton_zero_smul_set` `const_smul_of_ne_zero`
`const_vadd` 📖	mathematical	`MeasurableSet`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.preimage_vadd_neg` `MeasurableConstVAdd.measurable_const_vadd`

---