[Merged by Bors] - feat(AlgebraicGeometry): infinitesimal lifting criterion for formally unramified morphisms#35397

erdOne wants to merge 2 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

erdOne:erd1/formallyUnramifiedInfinitesimalerdOne/mathlib4:erd1/formallyUnramifiedInfinitesimalCopy head branch name to clipboard