[Merged by Bors] - feat(AlgebraicGeometry/Restrict): a few more restriction lemmas#39442

justus-springer wants to merge 7 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

justus-springer:justus/restrict_lemmasjustus-springer/mathlib4:justus/restrict_lemmasCopy head branch name to clipboard