Theorem Int.cast_smul_eq_zsmul

Modification history

2024-10-24 15:01

Mathlib/Algebra/Module/Defs.lean

chore(Algebra/Module): split `Defs` a bit further (#18169) …

Modified Int.cast_smul_eq_zsmul View on Github →

2024-08-06 08:17

Mathlib/Algebra/Module/Defs.lean

fix: `Int.cast_smul_eq_nsmul` → `Int.cast_smul_eq_zsmul` (#15528) …

Added Int.cast_smul_eq_zsmul View on Github →