Skip to content

[Merged by Bors] - doc(Algebra,AlgebraicGeometry): remove mathlib3 names in doc comments #26668

[Merged by Bors] - doc(Algebra,AlgebraicGeometry): remove mathlib3 names in doc comments

[Merged by Bors] - doc(Algebra,AlgebraicGeometry): remove mathlib3 names in doc comments #26668

Lint style

succeeded Apr 7, 2024 in 54s