RingTheory/Valuation/ValuationRing.lean

Stream: mathlib4

[Kim Morrison]

@Adam Topaz (or anyone else). The erws in the construction of instance : LE (ValueGroup A K) in Mathlib.RingTheory.Valuation.ValuationRing is fragile, and is breaking on nightly-testing. I have bigger problems on nightly-testing right now, but perhaps I can tempted someone to have a look at this file and see if it can be refactored so this proof runs with plain rw, no erw?

[Adam Topaz]

@Kim Morrison I have a fix. Shall I push directly to the branch?

[Adam Topaz]

Well, I pushed it to branch#AT-nightly-testing-valuation-fix . Feel free to merge as needed.

[Ruben Van de Velde]

I pushed it to nightly-testing, thanks!