Mathlib v3 is deprecated. Go to Mathlib v4

Theorem local_ring.is_unit_or_is_unit_of_is_unit_add

Modification history