mathlib

d8c87253 - feat(ring_theory,algebraic_geometry): Miscellaneous lemmas/def/typo corrections (#10307)