Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.is_integral_iff_is_irreducible_and_is_reduced

Modification history

2022-01-01 11:59
src/algebraic_geometry/properties.lean
feat(algebraic_geometry): The function field of an integral scheme (#11147)
Added algebraic_geometry.is_integral_iff_is_irreducible_and_is_reducedView on Github →