Commit 2026-03-06 13:45 20505103

chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain (#26872)

• try again
• added restrict0
• Update Range.lean
• removed min_imports
• added results on restrict
• added
• removed spaces
• removed imports
• min some imports
• Update Range.lean
• created v.restrict
• updated range
• wip
• some updates
• fixed linter
• wip
• created mul_iso
• Update Mathlib/Algebra/GroupWithZero/WithZero.lean
• Update Mathlib/Algebra/GroupWithZero/WithZero.lean
• Update Mathlib/Algebra/GroupWithZero/WithZero.lean
• build fix
• Update Mathlib/Algebra/GroupWithZero/WithZero.lean
• fixed apostrophes
• wip
• perhaps stopping here
• fixed build using Yakov' PR
• updated
• applied reviewer's suggestions
• Update Mathlib/Algebra/Order/GroupWithZero/WithZero.lean
• moving towards yakov's suggestion
• Update Mathlib/Algebra/GroupWithZero/Range.lean
• Update Mathlib/Algebra/Order/GroupWithZero/WithZero.lean
• removed extra basic
• Update Mathlib/Algebra/Order/GroupWithZero/Range.lean
• Update Mathlib/Algebra/GroupWithZero/Range.lean
• Update Range.lean
• Update Range.lean
• removed an equiv
• fixed something
• fix build
• Update Mathlib/Algebra/GroupWithZero/Range.lean
• Update Mathlib/Algebra/GroupWithZero/Range.lean
• commented withZeroUnits_mul
• first commit
• Update Mathlib/Algebra/GroupWithZero/WithZero.lean
• Update Mathlib/Algebra/GroupWithZero/WithZero.lean
• moved variable
• commented IsOrderedMonoid
• fixed build
• Update Mathlib/Algebra/GroupWithZero/Range.lean Yes, certainly much better, thanks.
• fixed HomClass
• addressed reviewer's comments
• one more comment
• one more comment
• Update Mathlib/Algebra/Order/GroupWithZero/Range.lean
• Update Mathlib/Algebra/Order/GroupWithZero/Range.lean
• Update Mathlib/Algebra/Order/GroupWithZero/Range.lean
• Update Mathlib/Algebra/GroupWithZero/Range.lean
• updated name
• Update Mathlib/Algebra/Order/GroupWithZero/Range.lean
• changed capitalization
• updated docstring
• renaming
• Update Mathlib/Algebra/GroupWithZero/Range.lean
• Update Mathlib/Algebra/Order/GroupWithZero/Range.lean
• fix build
• fix build+reviewer's comments
• fixed build
• removed simp
• reverted remove import
• Update Mathlib/Algebra/Order/GroupWithZero/Range.lean
• perhaps OK?
• fixed capitalization of OrderEmbedding
• mk_all
• fix build
• module
• Update Mathlib/Algebra/Order/GroupWithZero/Range.lean
• WIP
• WIP
• WIP
• fix DiscreteValuativeRel
• Update Mathlib/Algebra/GroupWithZero/Range.lean
• WIP
• WIP
• WIP
• WIP
• WIP
• WIP
• WIP
• WIP
• remove simp lemma
• WIP
• WIP
• WIP
• last files
• remove simp, add namespace
• fix
• remove decidable assumption
• more changes
• delete space
• some build fix
• add embedding_strictMono back
• delete orderEmbedding
• fix Valuation.Basic
• update ValuativeRel.Basic
• merging with some errors
• almost fix build
• tries
• add WithVal.valueGroup₀_equiv
• fill in proofs
• add strictMono statement
• closed strictMono_valueGroup₀_equiv
• progress on IsEquiv.uniformContinuous_equivWithVal
• WIP
• partial fixes
• another fix
• fix one error
• minigolf
• add exists_div_eq_of_unit
• added two lemmas while proving uniformContinuous_congr
• WIP
• prove IsEquiv.uniformContinuous_equiv
• advancing on congr
• added Salvatore's fix
• WIP
• delete old proof
• valuation_compare fixed? who knows
• WIP
• ops
• WIP
• delete sorries
• move lemma
• wip
• closed something
• removed useless lemma
• WIP
• with barmonoid
• WIP
• trying with inv
• WIP
• WIP
• fix name
• prove order preserving
• working on Kenny's prf
• WIP
• add orderMonoidIso
• delete comments
• wip
• fix file
• finish?
• fixing some build
• fixed other builds
• fix
• clean up
• some golfing
• first fifteen files are done
• second round of reviews
• fixed RatFunc notation
• applied one correction
• two deprecatsion and one ToD0
• added one reviewer's comment
• first suggestion by Salvatore
• Update Mathlib/Topology/Algebra/Valued/ValuedField.lean
• WIP
• one more leftover
• even more leftovers
• WIP
• restored MI's trials
• implemented more comments
• add valueGroup.mk
• fix merge issue
• add missing docstrings
• applied reviewer's comment
• applied comments
• review changes
• review changes

---