Commit 2022-01-06 07:55 f07f87e9
View on Github →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