Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-17 13:11 cf94743b

View on Github →

feat(ring_theory/finiteness): A morphism is finitely presented if the composition with a finite morphism is. (#15949)

Estimated changes

Modified src/ring_theory/adjoin/basic.lean

added theorem algebra.adjoin_adjoin_of_tower

Modified src/ring_theory/finiteness.lean

added theorem alg_hom.finite_presentation.of_comp_finite_type

added theorem algebra.finite_presentation.of_restrict_scalars_finite_presentation

added theorem ring_hom.finite_presentation.of_comp_finite_type