Theorem ValuativeRel.vlt_imp_vlt_of_vle_of_vle

Modification history

2026-06-07 02:12
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
feat(GRewrite): new `grw` implementation (#38318) …
Added ValuativeRel.vlt_imp_vlt_of_vle_of_vleView on Github →