Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-13 06:20 12b6b993

View on Github →

refactor(linear_algebra/affine_space): move def of slope to a new file (#11361) Also add a few trivial lemmas.

Estimated changes

deleted theorem eq_of_slope_eq_zero
deleted def slope
deleted theorem slope_comm
deleted theorem slope_def_field
deleted theorem slope_same
added theorem eq_of_slope_eq_zero
added def slope
added theorem slope_comm
added theorem slope_def_field
added theorem slope_def_module
added theorem slope_same
added theorem slope_sub_smul
added theorem slope_vadd_const
added theorem sub_smul_slope
added theorem sub_smul_slope_vadd