mathlib

381b9541 - feat(algebraic_geometry): An integral scheme is reduced and irreducible (#10733)

feat(algebraic_geometry): An integral scheme is reduced and irreducible (#10733) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>