Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-08 17:29 8fab107c

View on Github →

refactor(algebra/module): split of type constructions and move quotient, subtype and linear_map to their own theories in algebra/linear_algebra

Estimated changes

added theorem linear_map.add_app
added theorem linear_map.ext
added def linear_map.im
added def linear_map.ker
added theorem linear_map.map_add
added theorem linear_map.map_neg
added theorem linear_map.map_smul
added theorem linear_map.map_sub
added theorem linear_map.map_zero
added theorem linear_map.mem_im
added theorem linear_map.mem_ker
added theorem linear_map.neg_app
added theorem linear_map.smul_app
added theorem linear_map.sub_ker
added theorem linear_map.zero_app
added def linear_map
added theorem module.mul_app
added theorem module.one_app
added theorem add_val
added theorem neg_val
added theorem smul_val
added theorem sub_val
added theorem zero_val
deleted theorem is_submodule.add_val
deleted theorem is_submodule.neg_val
deleted theorem is_submodule.smul_val
deleted theorem is_submodule.sub_val
deleted theorem is_submodule.zero_val
deleted theorem linear_map.add_app
deleted theorem linear_map.ext
deleted def linear_map.im
deleted def linear_map.ker
deleted theorem linear_map.map_add
deleted theorem linear_map.map_neg
deleted theorem linear_map.map_smul
deleted theorem linear_map.map_sub
deleted theorem linear_map.map_zero
deleted theorem linear_map.mem_im
deleted theorem linear_map.mem_ker
deleted theorem linear_map.neg_app
deleted theorem linear_map.smul_app
deleted theorem linear_map.sub_ker
deleted theorem linear_map.zero_app
deleted def linear_map
deleted theorem module.mul_app
deleted theorem module.one_app
added def finsupp.filter
added theorem finsupp.support_filter