Theorem WithVal.ofVal_natCast

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.ofVal_natCastView on Github →