Theorem hasSum_coe_mul_geometric_of_norm_lt_1

Modification history