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

Commit

3 years ago

feat(ring_theory/finiteness): A morphism is finitely presented if the composition with a finite morphism is. (#15949) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author

erdOne

Parents

6d94ff7b

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

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