Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-29 05:05 b9e3dbba

View on Github →

feat(rat): give Q-algebra structure on field (#1628) also move around some declarations in rat.cast the only new declaration in that file is is_ring_hom_cast

Estimated changes

modified theorem rat.cast_add
modified theorem rat.cast_bit0
modified theorem rat.cast_bit1
modified theorem rat.cast_mul
modified theorem rat.cast_sub