Theorems · Theorem · sequences and series
multipliable_nat_add_iff
∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} (k : ℕ),
(Multipliable fun n => f (n + k)) ↔ Multipliable f- Cited by
- 5 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Finset.prodproof · cited by 2,356
- SummationFilter.unconditionalstatement · cited by 2,068
- Finset.rangeproof · cited by 1,341
- CommGroupstatement and proof · cited by 990
- IsTopologicalGroupstatement and proof · cited by 469
- Multipliablestatement · cited by 213
- Equiv.surjectiveproof · cited by 198
- Equiv.mulRightproof · cited by 21
- Function.Surjective.multipliable_iff_of_hasProd_iffproof · cited by 2
- hasProd_nat_add_iffproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- Multipliable.tprod_eq_zero_mulproof · cited by 2
- Multipliable.prod_mul_tprod_nat_addproof · cited by 1
- tprod_int_eq_zero_mul_tprod_pnatproof · cited by 1
- multipliable_pnat_iff_multipliable_natproof · cited by 0
- tendsto_prod_nat_addproof · cited by 0