Documentation

ABCExceptions.ForMathlib.Misc

theorem Finset.Ico_union_Icc_eq_Icc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} (h₁ : a b) (h₂ : b c) :
Ico a b Icc b c = Icc a c
theorem Finset.Ico_union_Icc_eq_Icc' {α : Type u_1} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] [LocallyFiniteOrder α] {a b c : α} (h₁ : a b) (h₂ : b c + 1) :
Ico a b Icc b c = Icc a c
theorem Nat.Icc_union_Icc_eq_Icc {a b c : } (h₁ : a b) (h₂ : b c) :
theorem Finset.prod_Icc_succ_bot {M : Type u_1} [CommMonoid M] {a b : } (hab : a b) (f : M) :
kIcc a b, f k = f a * kIcc (a + 1) b, f k
theorem Finset.sum_Icc_succ_bot {M : Type u_1} [AddCommMonoid M] {a b : } (hab : a b) (f : M) :
kIcc a b, f k = f a + kIcc (a + 1) b, f k
theorem prod_Icc_eq_prod_range_mul_prod_Icc {d : } {α : Type u_1} [CommMonoid α] {f : α} {t : } (ht : t d + 1) :
iFinset.Iic d, f i = (∏ iFinset.range t, f i) * iFinset.Icc t d, f i
theorem sum_Icc_eq_sum_range_add_sum_Icc {d : } {α : Type u_1} [AddCommMonoid α] {f : α} {t : } (ht : t d + 1) :
iFinset.Iic d, f i = iFinset.range t, f i + iFinset.Icc t d, f i
theorem coe_ofNat_eq_mod (m n : ) [NeZero m] :
@[simp]
theorem coe_ofNat_of_lt (m n : ) [NeZero m] (h : n < m) :