Range

📁 Source: Mathlib/Data/Multiset/Range.lean

Statistics

Metric	Count
Definitions range	1
Theorems card_range, coe_range, mem_range, nodup_range, notMem_range_self, range_add, range_add_eq_union, range_disjoint_map_add, range_le, range_subset, range_succ, range_zero, self_mem_range_succ	13
Total	14

Multiset

Definitions

Name	Category	Theorems
range 📖	CompOp	23 math math: Finset.range_val, range_add_eq_union, range_disjoint_map_add, Mathlib.Meta.Multiset.range_zero', card_range, coe_range, mem_range, range_subset, Mathlib.Meta.Multiset.range_succ', toFinset_range, notMem_range_self, range_add, range_le, Nat.multiset_Ico_map_mod, range_zero, nodup_range, range_succ, sort_range, bind_powerset_len, self_mem_range_succ, Polynomial.Chebyshev.roots_U_real_nodup, Polynomial.Chebyshev.roots_T_real_nodup, IsPrimitiveRoot.nthRoots_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_range 📖	mathematical	—	card range	—	—
coe_range 📖	mathematical	—	ofList range	—	—
mem_range 📖	mathematical	—	Multiset instMembership range	—	—
nodup_range 📖	mathematical	—	Nodup range	—	—
notMem_range_self 📖	mathematical	—	Multiset instMembership range	—	—
range_add 📖	mathematical	—	range Multiset instAdd map	—	—
range_add_eq_union 📖	mathematical	—	range Multiset instUnion map	—	range_add add_eq_union_iff_disjoint range_disjoint_map_add
range_disjoint_map_add 📖	mathematical	—	Disjoint Multiset instPartialOrder instOrderBot range map	—	disjoint_left mem_map LE.le.not_gt mem_coe range.eq_1
range_le 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder range	—	le_iff_subset nodup_range range_subset
range_subset 📖	mathematical	—	Multiset instHasSubset range	—	—
range_succ 📖	mathematical	—	range cons	—	range.eq_1 coe_add add_comm coe_singleton singleton_add
range_zero 📖	mathematical	—	range Multiset instZero	—	—
self_mem_range_succ 📖	mathematical	—	Multiset instMembership range	—	—

---

← Back to Index