Mathlib v3 is deprecated. Go to Mathlib v4

Theorem valuation_subring.coe_unit_group_to_residue_field_units_apply

Modification history