Theorem exists_wellFoundedGT

Modification history

2026-04-12 12:58
Mathlib/SetTheory/Cardinal/Order.lean
feat(RingTheory/MvPowerSeries/NoZeroDivisors): simplify the proof by adding `exists_wellFoundedGT` (#36892) …
Added exists_wellFoundedGTView on Github →