Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-24 08:35 46614b02

View on Github →

chore(ring_theory/power_series/well_known): generalize (#5491)

  • generalize power_series.exp, power_series.cos, and power_series.sin to a ℚ-algebra;
  • define alg_hom.mk';
  • rename alg_hom_nat to ring_hom.to_nat_alg_hom;
  • drop alg_hom_int (was equal to ring_hom.to_int_alg_hom);
  • add ring_hom.to_rat_alg_hom.

Estimated changes

added theorem alg_hom.coe_mk'
added def alg_hom.mk'
deleted def alg_hom_int
deleted def alg_hom_nat
modified theorem power_series.coeff_exp
modified def power_series.cos
modified def power_series.exp
modified theorem power_series.map_cos
modified theorem power_series.map_exp
modified theorem power_series.map_sin
modified def power_series.sin