Skip to content

Commit

Permalink
comment check
Browse files Browse the repository at this point in the history
  • Loading branch information
mariainesdff committed Jun 5, 2024
1 parent cbb6c94 commit fe8534a
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ namespace StronglySummable

variable [UniformSpace α] [UniformAddGroup α]

#check MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
--#check MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod

theorem hasProd_of_one_add (hf : StronglySummable f) :
HasProd (fun i => 1 + f i) hf.toStronglyMultipliable.prod := by
Expand Down

0 comments on commit fe8534a

Please sign in to comment.