Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:50 79ba61cc

View on Github →

feat(ring_theory/algebra): make algebra a class

Estimated changes

modified def alg_hom.comap
modified theorem alg_hom.commutes
modified def alg_hom.comp
modified theorem alg_hom.comp_apply
modified theorem alg_hom.comp_assoc
modified theorem alg_hom.comp_id
modified theorem alg_hom.ext
modified theorem alg_hom.id_apply
modified theorem alg_hom.id_comp
modified def alg_hom.to_linear_map
modified theorem alg_hom.to_linear_map_inj
modified structure alg_hom
modified def algebra.adjoin
modified def algebra.comap
modified theorem algebra.commutes
modified theorem algebra.left_comm
modified def algebra.lmul
modified theorem algebra.lmul_apply
modified def algebra.lmul_left
modified theorem algebra.lmul_left_apply
modified def algebra.lmul_right
modified theorem algebra.lmul_right_apply
modified theorem algebra.map_add
modified theorem algebra.map_mul
modified theorem algebra.map_neg
modified theorem algebra.map_one
modified theorem algebra.map_sub
modified theorem algebra.map_zero
modified theorem algebra.mem_bot
modified theorem algebra.mem_top
modified def algebra.of_id
modified theorem algebra.of_id_apply
deleted def algebra.polynomial
deleted def algebra.right
modified theorem algebra.smul_def
modified theorem algebra.smul_mul
modified def algebra.to_comap
modified theorem algebra.to_comap_apply
modified def algebra.to_top
deleted structure algebra
added def algebra_map
modified def mv_polynomial.aeval
modified theorem mv_polynomial.aeval_def
modified theorem mv_polynomial.eval_unique
modified def polynomial.aeval
modified theorem polynomial.aeval_def
modified theorem polynomial.eval_unique
modified theorem subalgebra.ext
modified theorem subalgebra.mem_coe
modified def subalgebra.val
modified structure subalgebra