Mathlib v3 is deprecated. Go to Mathlib v4

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