mathlib3

f07f87e9 - feat(ring_theory/power_series/basic): algebra, solving TODOs (#11267)

feat(ring_theory/power_series/basic): algebra, solving TODOs (#11267) `algebra (mv_polynomial σ R) (mv_power_series σ A)` `algebra (mv_power_series σ R) (mv_power_series σ A)` `algebra (polynomial R) (power_series A)` `algebra (power_series R) (power_series A)` `coe_to_mv_power_series.alg_hom` `coe_to_power_series.alg_hom` And API about the injectivity of coercions