Theorem WithVal.ofVal_ofNat

Modification history

2026-05-25 10:51
Mathlib/Topology/Algebra/Valued/WithVal.lean
perf(WithVal): avoid Equiv.ring (#39562)
Deleted WithVal.ofVal_ofNatView on Github →
2026-05-19 07:24
Mathlib/Topology/Algebra/Valued/WithVal.lean
feat(Valued/WithVal): missing rfl lemmas for field operations (#39563) …
Added WithVal.ofVal_ofNatView on Github →