Commit 2019-01-27 22:50 a0b6cae4

View on Github →

feat(ring_theory/algebra): define algebra over a commutative ring

Estimated changes

added def alg_hom.comap
added theorem alg_hom.commutes
added def alg_hom.comp
added theorem alg_hom.comp_apply
added theorem alg_hom.comp_assoc
added theorem alg_hom.comp_id
added theorem alg_hom.ext
added theorem alg_hom.id_apply
added theorem alg_hom.id_comp
added theorem alg_hom.map_add
added theorem alg_hom.map_mul
added theorem alg_hom.map_neg
added theorem alg_hom.map_one
added theorem alg_hom.map_sub
added theorem alg_hom.map_zero
added structure alg_hom
added def algebra.adjoin
added def algebra.comap
added theorem algebra.commutes
added structure algebra.core
added theorem algebra.left_comm
added def algebra.lmul
added theorem algebra.lmul_apply
added theorem algebra.map_add
added theorem algebra.map_mul
added theorem algebra.map_neg
added theorem algebra.map_one
added theorem algebra.map_sub
added theorem algebra.map_zero
added theorem algebra.mem_bot
added theorem algebra.mem_top
added def algebra.of_core
added def algebra.of_id
added theorem algebra.of_id_apply
added def algebra.right
added theorem algebra.smul_def
added theorem algebra.smul_mul
added def algebra.to_comap
added theorem algebra.to_comap_apply
added def algebra.to_top
added structure algebra
added def polynomial.aeval
added theorem polynomial.aeval_def
added theorem polynomial.eval_unique
added def subalgebra.comap
added theorem subalgebra.ext
added theorem subalgebra.mem_coe
added def subalgebra.under
added def subalgebra.val
added structure subalgebra