[Merged by Bors] - feat(AlgebraicGeometry/Birational): Birationality and rationality of schemes#39122

justus-springer wants to merge 34 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

justus-springer:justus/birationaljustus-springer/mathlib4:justus/birationalCopy head branch name to clipboard