Theorem coe_nat_zsmul

Modification history

2023-02-17 17:10
Mathlib/Data/Int/Basic.lean
feat: to_additive raises linter errors; nested to_additive (#1819) …
Deleted coe_nat_zsmulView on Github →
2022-12-04 13:00
Mathlib/Algebra/Ring/Basic.lean
feat: port algebra.ring.basic (#830) …
Modified coe_nat_zsmulView on Github →
2022-11-01 00:14
Mathlib/Algebra/Ring/Basic.lean
feat: port abel1 (#509) …
Added coe_nat_zsmulView on Github →