Theorem WithVal.ofVal_intCast

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_intCastView on Github →