mathlib
b599b58c - refactor(algebraic_geometry/*): Tidy up simp lemmas regarding `basic_open`s. (#17014)

Commit

3 years ago

refactor(algebraic_geometry/*): Tidy up simp lemmas regarding `basic_open`s. (#17014) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author

erdOne

Parents

0d580447

mathlib b599b58c - refactor(algebraic_geometry/*): Tidy up simp lemmas regarding `basic_open`s. (#17014)

mathlib
b599b58c - refactor(algebraic_geometry/*): Tidy up simp lemmas regarding `basic_open`s. (#17014)