Commit 2025-07-04 09:20 789b5d30

feat(WithZero): exp : ℤ → ℤᵐ⁰, log : ℤᵐ⁰ → ℤ (#24977) In valuation theory, valuations have codomain {0} ∪ {e ^ n | n : ℤ}, which we can formalise as ℤₘ₀ := WithZero (Multiplicative ℤ). It is important to be able to talk about the maps n ↦ e ^ n and e ^ n ↦ n. We define these as exp : ℤ → ℤₘ₀ and log : ℤₘ₀ → ℤ with junk value log 0 = 0. Junkless versions are defined as expEquiv : ℤ ≃ ℤₘ₀ˣ and logEquiv : ℤₘ₀ˣ ≃ ℤ.