Commit 2025-01-08 18:19 c8899bb8

View on Github →

feat(Ringtheory/DedekindDomain/AdicValuation); add mem_integers_of_valuation_le_one (#20523) A Lean 4 port of Junyan Xu's code here.

Estimated changes