Theorem Nat.addCommute_cast_one

Modification history

2026-06-09 14:25
Mathlib/Data/Nat/Cast/Commute.lean
feat: `Nat.cast` commutes with addition (#39157) …
Added Nat.addCommute_cast_oneView on Github →