Commit 2023-01-27 18:02 2ee69787

View on Github →

feat: port Algebra.Module.Submodule.Basic (#1888)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Submodule/Basic.lean

added theorem Submodule.carrier_inj

added theorem Submodule.coeSubtype

added theorem Submodule.coe_add

added theorem Submodule.coe_copy

added theorem Submodule.coe_eq_zero

added theorem Submodule.coe_mem

added theorem Submodule.coe_mk

added theorem Submodule.coe_restrictScalars

added theorem Submodule.coe_set_mk

added theorem Submodule.coe_smul

added theorem Submodule.coe_smul_of_tower

added theorem Submodule.coe_sum

added theorem Submodule.coe_toAddSubgroup

added theorem Submodule.coe_toAddSubmonoid

added theorem Submodule.coe_toSubMulAction

added theorem Submodule.coe_zero

added theorem Submodule.copy_eq

added theorem Submodule.ext

added theorem Submodule.injective_subtype

added theorem Submodule.mem_carrier

added theorem Submodule.mem_mk

added theorem Submodule.mem_toAddSubgroup

added theorem Submodule.mem_toAddSubmonoid

added theorem Submodule.mk_eq_zero

added theorem Submodule.mk_le_mk

added theorem Submodule.ne_zero_of_ortho

added theorem Submodule.not_mem_of_ortho

added def Submodule.restrictScalars

added def Submodule.restrictScalarsEmbedding

added def Submodule.restrictScalarsEquiv

added theorem Submodule.restrictScalars_inj

added theorem Submodule.restrictScalars_injective

added theorem Submodule.restrictScalars_mem

added theorem Submodule.restrictScalars_self

added theorem Submodule.smul_mem

added theorem Submodule.smul_mem_iff'

added theorem Submodule.smul_mem_iff

added theorem Submodule.smul_of_tower_mem

added theorem Submodule.sub_mem_iff_left

added theorem Submodule.sub_mem_iff_right

added theorem Submodule.subtype_apply

added theorem Submodule.sum_smul_mem

added def Submodule.toAddSubgroup

added theorem Submodule.toAddSubgroup_eq

added theorem Submodule.toAddSubgroup_injective

added theorem Submodule.toAddSubgroup_le

added theorem Submodule.toAddSubgroup_mono

added theorem Submodule.toAddSubgroup_strictMono

added theorem Submodule.toAddSubmonoid_eq

added theorem Submodule.toAddSubmonoid_injective

added theorem Submodule.toAddSubmonoid_le

added theorem Submodule.toAddSubmonoid_mono

added theorem Submodule.toAddSubmonoid_strictMono

added theorem Submodule.toSubMulAction_eq

added theorem Submodule.toSubMulAction_injective

added theorem Submodule.toSubMulAction_mono

added theorem Submodule.toSubMulAction_strictMono

added structure Submodule

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean