Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
is_reduced_of_injective
Modification history
2021-12-27 16:46
src/ring_theory/nilpotent.lean
feat(algebraic_geometry): Basic open set is empty iff section is zero in reduced schemes. (#11012)
Added
is_reduced_of_injective
View on Github →