Commit 2023-05-22 18:54 d22d5a02

View on Github →

feat: port RingTheory.PowerSeries.WellKnown (#4215)

depends on: #4167

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/PowerSeries/WellKnown.lean

added theorem PowerSeries.coeff_cos_bit0

added theorem PowerSeries.coeff_cos_bit1

added theorem PowerSeries.coeff_exp

added theorem PowerSeries.coeff_invUnitsSub

added theorem PowerSeries.coeff_sin_bit0

added theorem PowerSeries.coeff_sin_bit1

added theorem PowerSeries.constantCoeff_exp

added theorem PowerSeries.constantCoeff_invUnitsSub

added def PowerSeries.cos

added def PowerSeries.exp

added theorem PowerSeries.exp_mul_exp_eq_exp_add

added theorem PowerSeries.exp_mul_exp_neg_eq_one

added theorem PowerSeries.exp_pow_eq_rescale_exp

added theorem PowerSeries.exp_pow_sum

added def PowerSeries.invUnitsSub

added theorem PowerSeries.invUnitsSub_mul_X

added theorem PowerSeries.invUnitsSub_mul_sub

added theorem PowerSeries.map_cos

added theorem PowerSeries.map_exp

added theorem PowerSeries.map_invUnitsSub

added theorem PowerSeries.map_sin

added def PowerSeries.sin