Mathlib v3 is deprecated. Go to Mathlib v4

Theorem valuation.mem_unit_group_iff

Modification history

2022-09-08 20:32

src/ring_theory/valuation/valuation_subring.lean

feat(ring_theory/dedekind_domain/integer_unit): define S-integers and S-units (#15646)

Added valuation.mem_unit_group_iff View on Github →