Theorem WithVal.toVal_nnratCast

Modification history

2026-05-19 07:24
Mathlib/Topology/Algebra/Valued/WithVal.lean
feat(Valued/WithVal): missing rfl lemmas for field operations (#39563) …
Added WithVal.toVal_nnratCastView on Github →