Commit 2023-03-08 20:31 d1716a32

View on Github →

feat: port LinearAlgebra.AffineSpace.Slope (#2728)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/Slope.lean

added theorem AffineMap.slope_comp

added theorem LinearMap.slope_comp

added theorem eq_of_slope_eq_zero

added theorem lineMap_slope_lineMap_slope_lineMap

added theorem lineMap_slope_slope_sub_div_sub

added def slope

added theorem slope_comm

added theorem slope_def_field

added theorem slope_def_module

added theorem slope_fun_def

added theorem slope_fun_def_field

added theorem slope_same

added theorem slope_sub_smul

added theorem slope_vadd_const

added theorem sub_div_sub_smul_slope_add_sub_div_sub_smul_slope

added theorem sub_smul_slope

added theorem sub_smul_slope_vadd