Commit 2026-05-19 07:24 ec097dff

View on Github →

feat(Valued/WithVal): missing rfl lemmas for field operations (#39563) This adds the missing lemmas for (nat|int|nnrat|rat)Cast, zpow, and ofNat. These were found while attempting a refactor to use Function.Injective.field in #39562.

Estimated changes

added theorem WithVal.ofVal_intCast
added theorem WithVal.ofVal_natCast
added theorem WithVal.ofVal_ofNat
added theorem WithVal.ofVal_ratCast
added theorem WithVal.ofVal_zpow
added theorem WithVal.toVal_intCast
added theorem WithVal.toVal_natCast
added theorem WithVal.toVal_ofNat
added theorem WithVal.toVal_ratCast
added theorem WithVal.toVal_zpow