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 →