Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-05 17:24 dcfb9a01

View on Github →

refactor(algebra/module): add is_linear_map as predicate

Estimated changes

Modified algebra/module.lean

added theorem is_linear_map.comp

added theorem is_linear_map.id

added theorem is_linear_map.map_add

added theorem is_linear_map.map_neg

added theorem is_linear_map.map_smul_left

added theorem is_linear_map.map_smul_right

added theorem is_linear_map.map_sub

added theorem is_linear_map.map_sum

added theorem is_linear_map.map_zero

added theorem is_linear_map.neg

added theorem is_linear_map.sub

added theorem is_linear_map.sum

added theorem is_linear_map.zero

added structure is_linear_map

added theorem is_submodule.Inter_submodule

added theorem is_submodule.is_linear_map_subtype_mk

added theorem is_submodule.is_linear_map_subtype_val

modified theorem is_submodule.sub_val

modified theorem linear_map.add_app

modified theorem linear_map.ext

modified def linear_map.im

added theorem linear_map.is_linear_map_coe

modified def linear_map.ker

added theorem linear_map.map_add

deleted theorem linear_map.map_add_app

modified theorem linear_map.map_neg

added theorem linear_map.map_smul

deleted theorem linear_map.map_smul_app

modified theorem linear_map.map_sub

modified theorem linear_map.map_zero

modified theorem linear_map.mem_im

modified theorem linear_map.neg_app

modified theorem linear_map.smul_app

modified theorem linear_map.zero_app

added def linear_map

deleted structure linear_map

deleted def module.endomorphism_ring

modified def module.general_linear_group

modified theorem module.mul_app

modified theorem module.one_app

added theorem set.sInter_eq_Inter

added theorem smul_eq_mul