Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-06 15:42 bc2bcac7

View on Github →

chore(algebra/module): Move submodule to its own file (#3696)

Estimated changes

Modified src/algebra/module/basic.lean

deleted theorem submodule.add_mem

deleted theorem submodule.add_mem_iff_left

deleted theorem submodule.add_mem_iff_right

deleted theorem submodule.coe_add

deleted theorem submodule.coe_eq_coe

deleted theorem submodule.coe_eq_zero

deleted theorem submodule.coe_injective

deleted theorem submodule.coe_mem

deleted theorem submodule.coe_mk

deleted theorem submodule.coe_neg

deleted theorem submodule.coe_set_eq

deleted theorem submodule.coe_smul

deleted theorem submodule.coe_sort_coe

deleted theorem submodule.coe_sub

deleted theorem submodule.coe_to_add_subgroup

deleted theorem submodule.coe_zero

deleted theorem submodule.ext'_iff

deleted theorem submodule.ext

deleted theorem submodule.mem_coe

deleted theorem submodule.mk_eq_zero

deleted theorem submodule.neg_mem

deleted theorem submodule.neg_mem_iff

deleted theorem submodule.smul_mem

deleted theorem submodule.smul_mem_iff'

deleted theorem submodule.smul_mem_iff

deleted theorem submodule.sub_mem

deleted theorem submodule.subtype_apply

deleted theorem submodule.subtype_eq_val

deleted theorem submodule.sum_mem

deleted theorem submodule.sum_smul_mem

deleted def submodule.to_add_subgroup

deleted theorem submodule.to_add_submonoid_eq

deleted theorem submodule.to_add_submonoid_injective

deleted theorem submodule.zero_mem

deleted structure submodule

deleted def subspace

Modified src/algebra/module/default.lean

Created src/algebra/module/submodule.lean

added theorem submodule.add_mem

added theorem submodule.add_mem_iff_left

added theorem submodule.add_mem_iff_right

added theorem submodule.coe_add

added theorem submodule.coe_eq_coe

added theorem submodule.coe_eq_zero

added theorem submodule.coe_injective

added theorem submodule.coe_mem

added theorem submodule.coe_mk

added theorem submodule.coe_neg

added theorem submodule.coe_set_eq

added theorem submodule.coe_smul

added theorem submodule.coe_sort_coe

added theorem submodule.coe_sub

added theorem submodule.coe_to_add_subgroup

added theorem submodule.coe_zero

added theorem submodule.ext'_iff

added theorem submodule.ext

added theorem submodule.mem_coe

added theorem submodule.mk_eq_zero

added theorem submodule.neg_mem

added theorem submodule.neg_mem_iff

added theorem submodule.smul_mem

added theorem submodule.smul_mem_iff'

added theorem submodule.smul_mem_iff

added theorem submodule.sub_mem

added theorem submodule.subtype_apply

added theorem submodule.subtype_eq_val

added theorem submodule.sum_mem

added theorem submodule.sum_smul_mem

added def submodule.to_add_subgroup

added theorem submodule.to_add_submonoid_eq

added theorem submodule.to_add_submonoid_injective

added theorem submodule.zero_mem

added structure submodule

added def subspace

Modified src/linear_algebra/basic.lean