mathlib3
46614b02 - chore(ring_theory/power_series/well_known): generalize (#5491)

Commit
5 years ago
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`.
Author
Parents
Loading