Commit 2026-01-25 15:24 7f1afc1e

View on Github →

feat(ValuationSubring): eq_top_iff + qol changes (#33604) Given a A : ValuationSubring K, this PR adds the lemma eq_top_iff : A = ⊤ ↔ ¬ A.valuation.IsNontrivial. I have also made some small quality of life changes:

  1. Added other forms of the basic rewrite lemmas with Valuation.IsEquiv:
  • eq_zero
  • one_le_iff_one_le
  • neq_one_iff_neq_one
  • one_lt_iff_one_lt
  • removed : ne_zero
  1. Reorganized section following the IsEquiv namespace block in Valuation.Basic
  2. Added lemmas (h : v.IsEquiv v') : v.IsNontrivial ↔ v'.IsNontrivial
  • isNontrivial_of_isEquiv
  • isNontrivial_iff_isEquiv_isNontrivial
  1. Added simp tags
  2. Added simp lemmas
  • isNontrivial_valuationSubring_valuation_iff

Estimated changes

modified theorem Valuation.IsEquiv.ne_zero
modified theorem Valuation.IsEquiv.pos_iff
modified theorem Valuation.isEquiv_tfae