Mathlib Changelog
Changelog
About
Github
Commit
2020-10-26 18:39
877a20e3
View on Github →
feat(ring_theory/finiteness): some finiteness notions in commutative algebra (
#4634
)
Estimated changes
Modified
src/data/mv_polynomial/basic.lean
Modified
src/ring_theory/adjoin.lean
Created
src/ring_theory/finiteness.lean
added
theorem
alg_hom.finite.comp
added
theorem
alg_hom.finite.finite_type
added
theorem
alg_hom.finite.id
added
theorem
alg_hom.finite.of_surjective
added
def
alg_hom.finite
added
theorem
alg_hom.finite_type.comp
added
theorem
alg_hom.finite_type.comp_surjective
added
theorem
alg_hom.finite_type.id
added
theorem
alg_hom.finite_type.of_surjective
added
def
alg_hom.finite_type
added
theorem
algebra.finite_type.equiv
added
theorem
algebra.finite_type.of_surjective
added
theorem
algebra.finite_type.self
added
theorem
algebra.finite_type.trans
added
def
algebra.finite_type
added
theorem
module.finite.equiv
added
theorem
module.finite.of_injective
added
theorem
module.finite.of_surjective
added
theorem
module.finite.trans
added
def
module.finite
added
theorem
module.finite_def
added
theorem
ring_hom.finite.comp
added
theorem
ring_hom.finite.finite_type
added
theorem
ring_hom.finite.id
added
theorem
ring_hom.finite.of_surjective
added
def
ring_hom.finite
added
theorem
ring_hom.finite_type.comp
added
theorem
ring_hom.finite_type.comp_surjective
added
theorem
ring_hom.finite_type.id
added
theorem
ring_hom.finite_type.of_surjective
added
def
ring_hom.finite_type