Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-28 19:59 b39d6d8a

View on Github →

feat(*) refactor module

Estimated changes

Modified src/algebra/module.lean

modified def is_linear_map.mk'

modified theorem is_linear_map.mk'_apply

modified def linear_map.comp

modified theorem linear_map.comp_apply

modified theorem linear_map.ext

modified theorem linear_map.ext_iff

modified def linear_map.id

modified theorem linear_map.is_linear

modified structure linear_map

modified theorem one_smul

modified theorem submodule.neg_mem

modified structure submodule

modified theorem zero_smul

Modified src/algebra/pi_instances.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/data/dfinsupp.lean

modified def dfinsupp.lmk

modified theorem dfinsupp.lmk_apply

modified def dfinsupp.lsingle

modified theorem dfinsupp.lsingle_apply

modified theorem dfinsupp.mk_smul

Modified src/data/finsupp.lean

modified def finsupp.to_has_scalar'

Modified src/linear_algebra/basic.lean

deleted theorem classical.some_spec3

modified theorem linear_equiv.apply_symm_apply

modified theorem linear_equiv.coe_apply

modified def linear_equiv.congr_right

modified theorem linear_equiv.of_bijective_apply

modified def linear_equiv.of_linear

modified theorem linear_equiv.of_linear_apply

modified theorem linear_equiv.of_linear_symm_apply

modified def linear_equiv.of_top

modified def linear_equiv.refl

modified def linear_equiv.symm

modified theorem linear_equiv.symm_apply_apply

modified def linear_equiv.trans

modified structure linear_equiv

modified def linear_map.cod_restrict

modified theorem linear_map.cod_restrict_apply

modified theorem linear_map.comap_cod_restrict

modified theorem linear_map.comap_injective

modified theorem linear_map.comap_le_comap_iff

modified theorem linear_map.comap_map_eq

modified theorem linear_map.comap_map_eq_self

modified theorem linear_map.comap_pair_prod

modified theorem linear_map.comp_id

modified def linear_map.congr_right

modified def linear_map.copair

modified theorem linear_map.copair_apply

modified theorem linear_map.copair_inl

modified theorem linear_map.copair_inl_inr

modified theorem linear_map.copair_inr

modified theorem linear_map.disjoint_ker'

modified theorem linear_map.disjoint_ker

modified def linear_map.endomorphism_ring

modified def linear_map.fst

modified theorem linear_map.fst_apply

modified theorem linear_map.fst_eq_copair

modified theorem linear_map.fst_pair

modified theorem linear_map.id_comp

modified theorem linear_map.inj_of_disjoint_ker

modified def linear_map.inl

modified theorem linear_map.inl_apply

modified theorem linear_map.inl_eq_pair

modified def linear_map.inr

modified theorem linear_map.inr_apply

modified theorem linear_map.inr_eq_pair

modified def linear_map.inverse

modified def linear_map.ker

modified theorem linear_map.ker_comp

modified theorem linear_map.ker_eq_bot

modified theorem linear_map.ker_eq_top

modified theorem linear_map.ker_id

modified theorem linear_map.ker_le_ker_comp

modified theorem linear_map.ker_zero

modified theorem linear_map.le_ker_iff_map

modified theorem linear_map.map_cod_restrict

modified theorem linear_map.map_comap_eq

modified theorem linear_map.map_comap_eq_self

modified theorem linear_map.map_copair_prod

modified theorem linear_map.map_injective

modified theorem linear_map.map_le_map_iff

modified theorem linear_map.mem_ker

modified theorem linear_map.mem_range

modified theorem linear_map.mul_app

modified theorem linear_map.one_app

modified def linear_map.pair

modified theorem linear_map.pair_apply

modified theorem linear_map.pair_fst_snd

modified def linear_map.range

modified theorem linear_map.range_coe

modified theorem linear_map.range_comp

modified theorem linear_map.range_comp_le_range

modified theorem linear_map.range_eq_top

modified theorem linear_map.range_id

modified theorem linear_map.range_le_iff_comap

modified def linear_map.smul_right

modified theorem linear_map.smul_right_apply

modified def linear_map.snd

modified theorem linear_map.snd_apply

modified theorem linear_map.snd_eq_copair

modified theorem linear_map.snd_pair

modified theorem linear_map.sub_mem_ker_iff

modified theorem linear_map.sum_apply

added def linear_map.sup_quotient_to_quotient_inf

modified theorem linear_map.zero_apply

modified def submodule.comap

modified theorem submodule.comap_bot

modified theorem submodule.comap_coe

modified theorem submodule.comap_comp

modified theorem submodule.comap_fst

modified theorem submodule.comap_liftq

modified theorem submodule.comap_mono

modified theorem submodule.comap_snd

modified theorem submodule.comap_top

modified theorem submodule.ker_inl

modified theorem submodule.ker_inr

modified theorem submodule.ker_liftq

modified theorem submodule.ker_liftq_eq_bot

modified theorem submodule.le_comap_map

modified def submodule.liftq

modified theorem submodule.liftq_apply

modified theorem submodule.liftq_mkq

modified def submodule.map

modified theorem submodule.map_bot

modified theorem submodule.map_coe

modified theorem submodule.map_comap_le

modified theorem submodule.map_comp

modified theorem submodule.map_inf_eq_map_inf_comap

modified theorem submodule.map_inl

modified theorem submodule.map_inr

modified theorem submodule.map_le_iff_le_comap

added theorem submodule.map_liftq

modified theorem submodule.map_mono

modified theorem submodule.map_top

modified def submodule.mapq

modified theorem submodule.mapq_apply

modified theorem submodule.mapq_mkq

modified theorem submodule.mem_comap

modified theorem submodule.mem_map

modified theorem submodule.mem_map_of_mem

modified theorem submodule.mem_span

modified theorem submodule.mem_span_insert'

modified theorem submodule.mem_span_insert

modified theorem submodule.mem_span_singleton

modified def submodule.mkq

modified def submodule.of_le

modified theorem submodule.prod_comap_inl

modified theorem submodule.prod_comap_inr

modified theorem submodule.prod_map_fst

modified theorem submodule.prod_map_snd

modified theorem submodule.range_fst

added theorem submodule.range_liftq

modified theorem submodule.range_snd

modified theorem submodule.span_Union

modified theorem submodule.span_empty

modified theorem submodule.span_eq

modified theorem submodule.span_eq_bot

modified theorem submodule.span_eq_of_le

modified theorem submodule.span_image

modified theorem submodule.span_induction

modified theorem submodule.span_insert_eq_span

modified theorem submodule.span_le

modified theorem submodule.span_mono

modified theorem submodule.span_singleton_eq_bot

modified theorem submodule.span_singleton_eq_range

modified theorem submodule.span_span

modified theorem submodule.span_union

modified theorem submodule.subset_span

Modified src/linear_algebra/basis.lean

modified theorem constr_add

modified theorem constr_basis

modified theorem constr_congr

modified theorem constr_eq

modified theorem constr_neg

modified theorem constr_range

modified theorem constr_self

modified theorem constr_sub

modified theorem constr_zero

modified theorem exists_is_basis

modified theorem exists_left_inverse_linear_map_of_injective

modified theorem exists_linear_independent

modified theorem exists_right_inverse_linear_map_of_surjective

modified theorem exists_subset_is_basis

modified theorem is_basis.ext

modified theorem is_basis.mem_span

modified theorem is_basis.repr_range

modified theorem is_basis.repr_supported

modified theorem is_basis.total_comp_repr

modified theorem is_basis.total_repr

modified def is_basis

modified theorem is_basis_empty

modified theorem is_basis_empty_bot

modified theorem is_basis_injective

modified theorem is_basis_span

modified theorem linear_equiv.is_basis

modified theorem linear_independent.disjoint_ker

modified theorem linear_independent.image

modified theorem linear_independent.inj_span_iff_inj

modified theorem linear_independent.insert

modified theorem linear_independent.mono

modified theorem linear_independent.of_image

modified def linear_independent.repr

modified theorem linear_independent.repr_eq

modified theorem linear_independent.repr_range

modified theorem linear_independent.repr_supported

modified theorem linear_independent.total_comp_repr

modified def linear_independent.total_equiv

modified theorem linear_independent.total_repr

modified theorem linear_independent.unique

modified theorem linear_independent_empty

modified theorem linear_independent_iff

modified theorem linear_independent_iff_not_mem_span

modified theorem linear_independent_iff_total_on

modified theorem linear_independent_singleton

modified theorem mem_span_insert_exchange

modified def module_equiv_lc

modified theorem zero_not_mem_of_linear_independent

Modified src/linear_algebra/dimension.lean

modified theorem dim_eq_injective

modified theorem dim_eq_surjective

modified theorem dim_le_injective

modified theorem dim_le_surjective

modified theorem dim_range_add_dim_ker

modified theorem dim_range_le

modified theorem dim_range_of_surjective

modified theorem dim_span

modified theorem is_basis.le_span

modified theorem is_basis.mk_eq_dim

modified theorem linear_equiv.dim_eq

modified theorem mk_eq_mk_of_basis

modified def rank

modified theorem rank_add_le

modified theorem rank_comp_le1

modified theorem rank_comp_le2

modified theorem rank_le_domain

modified theorem rank_le_range

Modified src/linear_algebra/direct_sum_module.lean

modified def direct_sum.lmk

modified def direct_sum.lof

modified theorem direct_sum.mk_smul

modified theorem direct_sum.of_smul

modified theorem direct_sum.to_module.ext

modified theorem direct_sum.to_module.unique

modified def direct_sum.to_module

modified theorem direct_sum.to_module_lof

Modified src/linear_algebra/linear_combination.lean

modified theorem lc.map_id

modified theorem lc.map_total

modified theorem lc.range_restrict_dom

modified def lc.restrict_dom

modified theorem lc.supported_empty

modified theorem lc.supported_univ

modified def lc.total_on

modified theorem lc.total_on_range

modified theorem lc.total_range

modified theorem linear_eq_on

modified theorem mem_span_iff_lc

modified theorem span_eq_map_lc

Modified src/linear_algebra/tensor_product.lean

modified def linear_map.compl₂

modified theorem linear_map.compl₂_apply

modified theorem linear_map.compr₂_apply

modified theorem linear_map.ext₂

modified theorem linear_map.flip_inj

modified def linear_map.lcomp

modified theorem linear_map.lcomp_apply

modified def linear_map.lflip

modified def linear_map.llcomp

modified theorem linear_map.llcomp_apply

modified theorem linear_map.map_smul₂

modified theorem tensor_product.add_tmul

modified def tensor_product.congr

modified def tensor_product.curry

modified theorem tensor_product.curry_apply

modified def tensor_product.direct_sum

modified theorem tensor_product.ext

modified def tensor_product.lcurry

modified theorem tensor_product.lcurry_apply

modified theorem tensor_product.lift.unique

modified theorem tensor_product.lift_aux.smul

modified def tensor_product.lift_aux

modified def tensor_product.map

modified theorem tensor_product.map_tmul

modified theorem tensor_product.neg_tmul

modified def tensor_product.smul.aux

modified theorem tensor_product.smul_tmul

modified def tensor_product.tmul

modified theorem tensor_product.tmul_add

modified theorem tensor_product.tmul_neg

modified theorem tensor_product.tmul_smul

modified theorem tensor_product.tmul_zero

modified def tensor_product.uncurry

modified theorem tensor_product.uncurry_apply

modified theorem tensor_product.zero_tmul

Modified src/measure_theory/outer_measure.lean

Modified src/ring_theory/algebra.lean

Modified src/ring_theory/ideal_operations.lean

modified theorem submodule.bot_smul

modified theorem submodule.span_smul_span

modified theorem submodule.top_smul

Modified src/ring_theory/ideals.lean

modified def ideal.span

Modified src/ring_theory/noetherian.lean

modified theorem is_noetherian_of_linear_equiv

modified theorem is_noetherian_of_surjective

modified def submodule.fg

Modified src/ring_theory/principal_ideal_domain.lean