Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-10 10:19 e7582631

View on Github →

refactor(ring_theory/algebra): use bundled homs, allow semirings (#2303) Fixes #2297 Build fails because of some class instance problems, asked on Zulip, no answer yet.

Estimated changes

modified theorem mv_polynomial.aeval_C
modified theorem mv_polynomial.aeval_def
modified theorem polynomial.aeval_C
modified theorem polynomial.aeval_def
modified theorem polynomial.degree_map
modified theorem polynomial.degree_map_le
modified theorem polynomial.map_div
modified theorem polynomial.map_div_by_monic
modified theorem polynomial.map_eq_zero
modified theorem polynomial.map_id
modified theorem polynomial.map_injective
modified theorem polynomial.map_map
modified theorem polynomial.map_mod
modified theorem polynomial.map_mod_by_monic
modified theorem polynomial.map_neg
modified theorem polynomial.map_sub
modified theorem polynomial.monic_map
modified theorem polynomial.nat_degree_map
modified theorem polynomial.splits_map_iff
modified theorem adjoin_root.eval₂_root
modified theorem adjoin_root.is_root_root
modified theorem alg_hom.commutes
modified theorem alg_hom.ext
deleted theorem alg_hom.id_to_linear_map
modified def algebra.comap
modified theorem algebra.commutes
modified theorem algebra.id.map_eq_self
modified theorem algebra.left_comm
deleted theorem algebra.map_add
deleted theorem algebra.map_mul
deleted theorem algebra.map_neg
deleted theorem algebra.map_one
deleted theorem algebra.map_sub
deleted theorem algebra.map_zero
modified theorem algebra.mem_bot
modified def algebra.of_id
modified theorem algebra.of_id_apply
deleted def algebra.of_ring_hom
modified theorem algebra.smul_def''
modified theorem algebra.smul_def
modified theorem algebra.to_comap_apply
modified def algebra_map
modified theorem subalgebra.range_le
modified theorem is_integral_algebra_map