Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int_smul_eq_gsmul

Modification history

2021-10-28 02:37

src/algebra/module/basic.lean

chore(*): rename gsmul to zsmul and gmultiples to zmultiples (#10010) …

Deleted int_smul_eq_gsmul View on Github →

2021-04-25 10:09

src/algebra/module/basic.lean

refactor(*): kill int multiplication diamonds (#7255) …

Added int_smul_eq_gsmul View on Github →