Mathlib v3 is deprecated. Go to Mathlib v4

Theorem rat.cast_injective

Modification history

2019-08-01 17:01

src/data/rat/basic.lean

feat(data/rat): refactor into smaller files and add documentation (#1284)

Modified rat.cast_injective View on Github →

2018-01-19 16:18

feat(data/real,*): supporting material for metric spaces

Added rat.cast_injective View on Github →