Theorem PowerSeries.mk_one_mul_one_sub_eq_one

Modification history