Range

Statistics

Metric	Count
Definitions	0
Theorems `disjoint_range_addLeftEmbedding`, `disjoint_range_addRightEmbedding`, `range_add`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_range_addLeftEmbedding` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `range` `map` `addLeftEmbedding` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid` `Nat.instAddCancelCommMonoid`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd`
`disjoint_range_addRightEmbedding` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `range` `map` `addRightEmbedding` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `IsCancelAdd.toIsLeftCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsCancelAdd.toIsRightCancelAdd` `addLeftEmbedding_eq_addRightEmbedding` `disjoint_range_addLeftEmbedding`
`range_add` 📖	mathematical	—	`range` `Finset` `instUnion` `map` `addLeftEmbedding` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid` `Nat.instAddCancelCommMonoid`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd` `union_val` `Multiset.range_add_eq_union`

---