Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.RingedSpace.is_unit_of_is_unit_germ

Modification history

2021-10-01 08:55
src/algebraic_geometry/ringed_space.lean
feat(algebraic_geometry/ringed_space): Define basic opens for ringed spaces. (#9358) …
Added algebraic_geometry.RingedSpace.is_unit_of_is_unit_germView on Github →