[Merged by Bors] - chore(AlgebraicGeometry): add LocallyRingedSpace.residue#41087

chrisflav wants to merge 2 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

chrisflav:lrs-residue-fixchrisflav/mathlib4:lrs-residue-fixCopy head branch name to clipboard