Theorem Nat.addCommute_cast

Modification history

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