Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:50 a0b6cae4

View on Github →

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

Estimated changes

Created src/ring_theory/algebra.lean

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 def alg_hom.to_linear_map

added theorem alg_hom.to_linear_map_apply

added theorem alg_hom.to_linear_map_inj

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 def algebra.lmul_left

added theorem algebra.lmul_left_apply

added def algebra.lmul_right

added theorem algebra.lmul_right_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.mv_polynomial

added def algebra.of_core

added def algebra.of_id

added theorem algebra.of_id_apply

added def algebra.of_subring

added def algebra.polynomial

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 is_ring_hom.to_ℤ_alg_hom

added def mv_polynomial.aeval

added theorem mv_polynomial.aeval_def

added theorem mv_polynomial.eval_unique

added def polynomial.aeval

added theorem polynomial.aeval_def

added theorem polynomial.eval_unique

added def ring.to_ℤ_algebra

added def subalgebra.comap

added theorem subalgebra.ext

added theorem subalgebra.mem_coe

added def subalgebra.to_submodule

added def subalgebra.under

added def subalgebra.val

added structure subalgebra