Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-07 17:30 085c0125

View on Github →

refactor(linear_algebra, ring_theory): rework submodules; move them to linear_algebra

Estimated changes

Modified data/set/basic.lean

added theorem set.image_eq_image

added theorem set.image_subset_image_iff

added theorem set.injective_image

added theorem set.preimage_eq_preimage

deleted theorem set.set_coe.exists

deleted theorem set.set_coe.forall

deleted theorem set.set_coe_cast

modified theorem set.set_coe_eq_subtype

added theorem set.surjective_preimage

added theorem set_coe.exists

added theorem set_coe.ext

added theorem set_coe.ext_iff

added theorem set_coe.forall

added theorem set_coe_cast

added theorem subtype.mem

Modified linear_algebra/linear_map_module.lean

deleted theorem classical.some_spec2

Modified linear_algebra/quotient_module.lean

added theorem quotient_module.coe_eq_zero

Created linear_algebra/submodule.lean

added theorem submodule.Union_set_of_directed

added theorem submodule.bot_set

added theorem submodule.coe_comap

added theorem submodule.coe_map

added def submodule.comap

added theorem submodule.comap_comp

added theorem submodule.comap_id

added theorem submodule.comap_map_eq

added def submodule.comap_quotient.order_iso

added def submodule.comap_quotient

added theorem submodule.ext

added theorem submodule.injective_comap

added theorem submodule.injective_map

added def submodule.lt_order_embedding

added def submodule.map

added theorem submodule.map_comp

added theorem submodule.map_id

added def submodule.map_subtype.le_order_embedding

added def submodule.map_subtype.order_iso

added def submodule.map_subtype

added theorem submodule.map_subtype_embedding_eq

added theorem submodule.map_subtype_subset

added theorem submodule.mem_coe

added theorem submodule.sInter_set

added def submodule.span

added theorem submodule.span_empty

added theorem submodule.span_subset_iff

added theorem submodule.span_union

added def submodule.submodule_lt_equiv

added theorem submodule.subset_comap_quotient

added theorem submodule.top_set

added structure {u

Modified linear_algebra/subtype_module.lean

deleted theorem add_val

deleted theorem is_linear_map_subtype_mk

deleted theorem is_linear_map_subtype_val

added theorem is_submodule.coe_add

added theorem is_submodule.coe_neg

added theorem is_submodule.coe_smul

added theorem is_submodule.coe_zero

added theorem is_submodule.is_linear_map_coe

deleted theorem is_submodule.is_linear_map_inclusion

added theorem is_submodule.is_linear_map_subtype_mk

added theorem is_submodule.is_linear_map_subtype_val

added theorem is_submodule.sub_val

deleted theorem neg_val

deleted theorem smul_val

deleted theorem sub_val

deleted theorem zero_val

Modified logic/basic.lean

added theorem classical.some_spec2

Modified order/basic.lean

added def linear_order.lift

added def partial_order.lift

added def preorder.lift

Deleted ring_theory/correspondence_theorem.lean

Modified ring_theory/noetherian.lean

deleted def submodule.univ

Deleted ring_theory/submodule.lean

deleted theorem submodule.Union_set_of_directed

deleted theorem submodule.bot_set

deleted theorem submodule.embedding_eq

deleted theorem submodule.eq

deleted theorem submodule.ext

deleted theorem submodule.mem_coe

deleted def submodule.pullback_injective_of_surjective

deleted def submodule.pushforward_injective_of_injective

deleted theorem submodule.sInter_set

deleted def submodule.span

deleted theorem submodule.span_empty

deleted theorem submodule.span_subset_iff

deleted theorem submodule.span_union

deleted theorem submodule.top_set

deleted structure {u

Modified set_theory/ordinal.lean