feat: port AlgebraicGeometry.Morphisms.RingHomProperties (#5663)

Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
leanprover-community · Jul 15, 2023 · 2922c5f · 2922c5f
1 parent 8d3c56c
commit 2922c5f
Show file tree

Hide file tree

Showing 3 changed files with 669 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -434,6 +434,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.Basic
 import Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
+import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
 import Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
 import Mathlib.AlgebraicGeometry.OpenImmersion.Basic
 import Mathlib.AlgebraicGeometry.OpenImmersion.Scheme