Mathlib v3 is deprecated. Go to Mathlib v4

Theorem rat_cast_smul_eq

Modification history

2021-10-08 07:33

src/algebra/module/basic.lean

feat(algebra/module/basic): `module rat E` is a subsingleton (#9570) …

Added rat_cast_smul_eq View on Github →