Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-06 03:28 d62cefd4

View on Github →

refactor(algebra/module): clean up PR commit

Estimated changes

Modified algebra/module.lean

deleted theorem eq_zero_of_add_self_eq

modified theorem linear_map.add_app

modified theorem linear_map.ext

deleted theorem linear_map.im.add_im

deleted theorem linear_map.im.mem_im

deleted theorem linear_map.im.neg_im

deleted theorem linear_map.im.smul_im

deleted theorem linear_map.im.zero_im

modified def linear_map.im

added theorem linear_map.inj_of_trivial_ker

deleted theorem linear_map.ker.inj_of_trivial_ker

deleted theorem linear_map.ker.ker_of_map_eq_map

deleted theorem linear_map.ker.mem_ker

deleted theorem linear_map.ker.sub_ker

modified def linear_map.ker

added theorem linear_map.ker_of_map_eq_map

modified theorem linear_map.map_add_app

modified theorem linear_map.map_neg

modified theorem linear_map.map_smul_app

modified theorem linear_map.map_sub

added theorem linear_map.mem_im

added theorem linear_map.mem_ker

modified theorem linear_map.neg_app

modified theorem linear_map.smul_app

added theorem linear_map.sub_ker

modified theorem linear_map.zero_app

modified structure linear_map

deleted theorem module.add_comp

deleted theorem module.comp_add

deleted theorem module.comp_app

deleted theorem module.comp_assoc

deleted theorem module.comp_id

modified def module.dual

modified def module.endomorphism_ring

modified def module.general_linear_group

deleted def module.id

deleted theorem module.id_app

deleted theorem module.id_comp

added theorem module.mul_app

added theorem module.one_app

modified theorem mul_smul

added theorem neg_one_smul

modified theorem neg_smul

modified theorem one_smul

modified theorem smul_left_distrib

modified theorem smul_neg

modified theorem smul_right_distrib

modified theorem smul_smul

modified theorem smul_sub_left_distrib

modified theorem smul_zero

modified theorem sub_smul_right_distrib

modified theorem submodule.add_val

added theorem submodule.neg

modified theorem submodule.neg_val

modified theorem submodule.smul_val

modified theorem submodule.sub

modified theorem submodule.zero_val

added def subspace

added def vector_space

modified theorem zero_smul

Modified algebra/ring.lean

added theorem units.ext

deleted def units.ext

added theorem units.inv_coe

modified theorem units.inv_mul

deleted theorem units.inv_val'

added theorem units.mul_coe

deleted theorem units.mul_four

added theorem units.mul_inv

deleted theorem units.mul_val

added theorem units.one_coe

deleted theorem units.one_val

added theorem units.val_coe

Deleted algebra/vector_space.lean

deleted def vector_space.dual

deleted def vector_space.general_linear_group