Theorem: QuadRing.gaussian_val_eq_top_iff_zero (ECTate/Algebra/QuadRing/Valuations.lean)

State before:
p : ℕ
gt1 : 1 < p
a : QuadRing ℤ 0 (-1)
⊢ gaussian_val p a = ⊤ ↔ a = 0
Tactic:
simp [gaussian_val, gt1, QuadRing.ext_iff]
State after:
no goals