Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-06 01:31 5cb7fb08

View on Github →

feat(algebra/vector_space): modules and vector spaces, linear spaces

Estimated changes

Modified algebra/module.lean

added theorem eq_zero_of_add_self_eq

added theorem linear_map.add_app

added theorem linear_map.ext

added theorem linear_map.im.add_im

added theorem linear_map.im.mem_im

added theorem linear_map.im.neg_im

added theorem linear_map.im.smul_im

added theorem linear_map.im.zero_im

added def linear_map.im

added theorem linear_map.ker.inj_of_trivial_ker

added theorem linear_map.ker.ker_of_map_eq_map

added theorem linear_map.ker.mem_ker

added theorem linear_map.ker.sub_ker

added def linear_map.ker

added theorem linear_map.map_add_app

added theorem linear_map.map_neg

added theorem linear_map.map_smul_app

added theorem linear_map.map_sub

added theorem linear_map.map_zero

added theorem linear_map.neg_app

added theorem linear_map.smul_app

added theorem linear_map.zero_app

added structure linear_map

added theorem module.add_comp

added theorem module.comp_add

added theorem module.comp_app

added theorem module.comp_assoc

added theorem module.comp_id

added def module.dual

added def module.endomorphism_ring

added def module.general_linear_group

added def module.id

added theorem module.id_app

added theorem module.id_comp

deleted def ring.to_module

added theorem smul_smul

added theorem submodule.add_val

added theorem submodule.neg_val

added theorem submodule.smul_val

added theorem submodule.sub

added theorem submodule.zero_val

Modified algebra/ring.lean

added def units.ext

added theorem units.inv_mul

added theorem units.inv_val'

added theorem units.mul_four

added theorem units.mul_val

added theorem units.one_val

added structure units

Created algebra/vector_space.lean

added def vector_space.dual

added def vector_space.general_linear_group