Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

Modified src/ring_theory/power_series/basic.lean

added theorem mv_polynomial.algebra_map_apply

modified theorem mv_polynomial.coe_add

added theorem mv_polynomial.coe_def

added theorem mv_polynomial.coe_eq_one_iff

added theorem mv_polynomial.coe_eq_zero_iff

added theorem mv_polynomial.coe_inj

added theorem mv_polynomial.coe_injective

modified theorem mv_polynomial.coe_mul

added def mv_polynomial.coe_to_mv_power_series.alg_hom

added theorem mv_polynomial.coe_to_mv_power_series.alg_hom_apply

added theorem mv_polynomial.coe_to_mv_power_series.ring_hom_apply

modified theorem mv_polynomial.coeff_coe

added theorem mv_power_series.algebra_map_apply''

added theorem mv_power_series.algebra_map_apply'

modified theorem polynomial.coe_add

added theorem polynomial.coe_def

added theorem polynomial.coe_eq_one_iff

added theorem polynomial.coe_eq_zero_iff

added theorem polynomial.coe_inj

added theorem polynomial.coe_injective

modified theorem polynomial.coe_mul

added def polynomial.coe_to_power_series.alg_hom

added theorem polynomial.coe_to_power_series.alg_hom_apply

modified def polynomial.coe_to_power_series.ring_hom

added theorem polynomial.coe_to_power_series.ring_hom_apply

modified theorem polynomial.coeff_coe

added theorem power_series.algebra_map_apply''

added theorem power_series.algebra_map_apply'

added theorem power_series.map_C

added theorem power_series.map_X