Mathlib Changelog
v3
Changelog
About
Github
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