Commit 2026-04-12 12:58 c290b55c

feat(RingTheory/MvPowerSeries/NoZeroDivisors): simplify the proof by adding exists_wellFoundedGT (#36892) Clean up unwanted declarations regarding to well-orderings.

• add exists_wellFoundedGTthat gives a linear ordering that satisfies WellFoundedGT
• rename exists_wellOrder to exists_wellFoundedLT, deprecate the previous name, and add to_dual existing to relate the two functions.
• adjust at a handful places, in particular in the proof of MvPowerSeries.NoZeroDivisors that the power series rings over a ring without zero divisors has no zero divisors, where the opposite of a “anti-well ordering” was needed.
• deprecate LinearOrder.swap which abuses defeq (and was only used once for that proof). Ref. #mathlib4 > help in RingTheory.MvPowerSeries.NeZeroDivisors