Theorem Nat.cast_add_one_comm

Modification history

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