theorem aux_false_of_forall_le_neg_nat (b' : Multiplicative ℤ) (h : ∀ (n : ℕ), Multiplicative.toAdd b' ≤ -↑n) : False

Auxiliary lemma: no element of Multiplicative ℤ can satisfy b'.toAdd ≤ -n for every natural number $n$, since taking $n$ large enough produces a contradiction.

theorem aux_eq_of_iff_le_neg_nat (x y : ℤ) (hx : x ≤ 0) (hy : y ≤ 0) (h : ∀ (n : ℕ), x ≤ -↑n ↔ y ≤ -↑n) : x = y

Two non-positive integers $x, y$ are equal whenever they satisfy the same family of inequalities $x \le -n \iff y \le -n$ for all $n \in \mathbb{N}$.

theorem WithZero.eq_of_le_exp_neg_iff {a b : WithZero (Multiplicative ℤ)} (ha : a ≤ 1) (hb : b ≤ 1) (h : ∀ (n : ℕ), a ≤ exp (-↑n) ↔ b ≤ exp (-↑n)) : a = b

Two elements $a, b \le 1$ of $\mathbb{Z}^{\mathrm{m}\circ}$ are equal iff they admit the same family of upper bounds $a \le \exp(-n) \iff b \le \exp(-n)$ for all natural $n$.

theorem mem_equivOfRingEquiv_pow_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (e : R ≃+* R) (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) (n : ℕ) : r ∈ ((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv e) v).asIdeal ^ n ↔ e.symm r ∈ v.asIdeal ^ n

For a ring automorphism $e$ of a Dedekind domain $R$ and a height-one prime $v$, an element $r$ lies in $(\mathrm{equivOfRingEquiv}\,e\,v)^n$ iff $e^{-1}(r)$ lies in $v^n$.

theorem intValuation_equivOfRingEquiv {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (e : R ≃+* R) (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : v.intValuation (e.symm r) = ((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv e) v).intValuation r

Compatibility of the $v$-adic integer valuation with a ring automorphism: the valuation at the transported prime $\mathrm{equivOfRingEquiv}\,e\,v$ applied to $r$ equals the original valuation at $v$ applied to $e^{-1}(r)$.