Theorem Valuation.Integers.isUnit_of_one'

Modification history

2024-07-27 08:25

Mathlib/RingTheory/Valuation/Integers.lean

chore: robustifying for debug.byAsSorry (part 10) (#15164)

Modified Valuation.Integers.isUnit_of_one'View on Github →

2024-07-03 09:27

Mathlib/RingTheory/Valuation/Integers.lean

feat (RingTheory/Valuation) : add lemmas about valuations and notations for valued (#13533) …

Added Valuation.Integers.isUnit_of_one'View on Github →