Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-10 11:14 43d3dee0

View on Github →

chore(linear_algebra): rename type variables (#1521)

  • doc(linear_algebra/basis): add doc
  • doc(linear_algebra/basis): shorten docstrings
  • refactor(linear_algebra/basis): rename type vars
  • style(linear_algebra/basic): change variable names
  • chore(linear_algebra/dimension): rename type variables
  • remove commented code
  • style(linear_algebra/bilinear_form): change variable names
  • style(linear_algebra/direct_sum_module): change variable names
  • style(linear_algebra/matrix): change variable names
  • Rename variables in finsupp_vector_space.lean
  • style(linear_algebra/sesquilinear_form): change variable names
  • style(linear_algebra/tensor_product): change variable names
  • change kappas to bb k's
  • style(linear_algebra/finsupp): change variable names
  • change universe levels
  • change bb k to K

Estimated changes

modified def equiv.to_linear_equiv
modified theorem finset.smul_sum
modified theorem finsupp.smul_sum
modified theorem linear_equiv.coe_apply
modified def linear_equiv.conj
modified theorem linear_equiv.ext
modified def linear_equiv.of_top
modified theorem linear_equiv.of_top_apply
modified def linear_equiv.refl
modified def linear_equiv.symm
modified def linear_equiv.trans
modified structure linear_equiv
modified theorem linear_map.add_apply
modified theorem linear_map.comap_injective
modified theorem linear_map.comap_map_eq
modified theorem linear_map.comap_pair_prod
modified theorem linear_map.comp_assoc
modified theorem linear_map.comp_smul
modified theorem linear_map.comp_zero
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 def linear_map.diag
modified theorem linear_map.disjoint_inl_inr
modified theorem linear_map.disjoint_ker'
modified theorem linear_map.disjoint_ker
modified theorem linear_map.finsupp_sum
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.infi_ker_proj
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_cod_restrict
modified theorem linear_map.ker_comp
modified theorem linear_map.ker_eq_bot'
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_pair
modified theorem linear_map.ker_pi
modified theorem linear_map.ker_smul'
modified theorem linear_map.ker_smul
modified theorem linear_map.ker_std_basis
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_copair_prod
modified theorem linear_map.map_injective
modified theorem linear_map.map_le_map_iff
modified theorem linear_map.map_le_range
modified theorem linear_map.mem_ker
modified theorem linear_map.mem_range
modified theorem linear_map.mul_app
modified theorem linear_map.neg_apply
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.pi
modified theorem linear_map.pi_apply
modified theorem linear_map.pi_comp
modified theorem linear_map.pi_eq_zero
modified theorem linear_map.pi_zero
modified def linear_map.prod
modified theorem linear_map.prod_eq_sup_map
modified def linear_map.proj
modified theorem linear_map.proj_apply
modified theorem linear_map.proj_pi
modified def linear_map.range
modified theorem linear_map.range_coe
modified theorem linear_map.range_comp
modified theorem linear_map.range_eq_top
modified theorem linear_map.range_id
modified theorem linear_map.range_le_bot_iff
modified theorem linear_map.range_smul'
modified theorem linear_map.range_smul
modified theorem linear_map.range_zero
modified theorem linear_map.smul_apply
modified theorem linear_map.smul_comp
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 def linear_map.std_basis
modified theorem linear_map.std_basis_apply
modified theorem linear_map.std_basis_ne
modified theorem linear_map.std_basis_same
modified theorem linear_map.sub_apply
modified theorem linear_map.sub_mem_ker_iff
modified theorem linear_map.sum_apply
modified theorem linear_map.update_apply
modified theorem linear_map.zero_apply
modified theorem linear_map.zero_comp
modified theorem submodule.Inf_coe
modified theorem submodule.add_eq_sup
modified theorem submodule.bot_coe
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_inf
modified theorem submodule.comap_infi
modified theorem submodule.comap_liftq
modified theorem submodule.comap_mono
modified theorem submodule.comap_smul'
modified theorem submodule.comap_smul
modified theorem submodule.comap_snd
modified theorem submodule.comap_top
modified theorem submodule.comap_zero
modified theorem submodule.disjoint_def
modified theorem submodule.eq_top_iff'
modified theorem submodule.gc_map_comap
modified theorem submodule.inf_coe
modified theorem submodule.infi_coe
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.ker_of_le
modified theorem submodule.le_comap_map
modified theorem submodule.le_comap_mkq
modified theorem submodule.le_def'
modified theorem submodule.le_def
modified def submodule.liftq
modified theorem submodule.liftq_apply
modified theorem submodule.liftq_mkq
modified theorem submodule.linear_eq_on
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_inl
modified theorem submodule.map_inr
modified theorem submodule.map_liftq
modified theorem submodule.map_mono
modified theorem submodule.map_smul'
modified theorem submodule.map_smul
modified theorem submodule.map_subtype_le
modified theorem submodule.map_sup
modified theorem submodule.map_supr
modified theorem submodule.map_top
modified theorem submodule.map_zero
modified def submodule.mapq
modified theorem submodule.mapq_apply
modified theorem submodule.mapq_mkq
modified theorem submodule.mem_bot
modified theorem submodule.mem_comap
modified theorem submodule.mem_inf
modified theorem submodule.mem_infi
modified theorem submodule.mem_map
modified theorem submodule.mem_map_of_mem
modified theorem submodule.mem_prod
modified theorem submodule.mem_span
modified theorem submodule.mem_span_insert'
modified theorem submodule.mem_span_insert
modified theorem submodule.mem_supr_of_mem
modified theorem submodule.mem_top
modified def submodule.mkq
modified theorem submodule.mkq_apply
modified def submodule.of_le
modified theorem submodule.of_le_apply
modified def submodule.prod
modified theorem submodule.prod_bot
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.prod_mono
modified theorem submodule.prod_top
modified def submodule.quotient.mk
modified theorem submodule.quotient.mk_eq_mk
modified theorem submodule.range_fst
modified theorem submodule.range_liftq
modified theorem submodule.range_of_le
modified theorem submodule.range_snd
modified def submodule.span
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_le
modified theorem submodule.span_mono
modified theorem submodule.span_prod_le
modified theorem submodule.span_span
modified theorem submodule.span_union
modified theorem submodule.span_univ
modified theorem submodule.subset_span
modified theorem submodule.top_coe
modified theorem submodule.zero_eq_bot
modified theorem constr_add
modified theorem constr_basis
modified theorem constr_eq
modified theorem constr_neg
modified theorem constr_range
modified theorem constr_self
modified theorem constr_smul
modified theorem constr_sub
modified theorem constr_zero
modified theorem disjoint_span_singleton
modified def equiv_fun_basis
modified def equiv_of_is_basis
modified theorem exists_is_basis
modified theorem exists_linear_independent
modified theorem exists_subset_is_basis
modified theorem is_basis.comp
modified def is_basis.constr
modified theorem is_basis.constr_apply
modified theorem is_basis.ext
modified theorem is_basis.injective
modified theorem is_basis.mem_span
modified def is_basis.repr
modified theorem is_basis.repr_range
modified theorem is_basis.repr_total
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_inl_union_inr
modified theorem is_basis_singleton_one
modified theorem is_basis_span
modified theorem le_of_span_le_span
modified theorem linear_equiv.is_basis
modified theorem linear_independent.image
modified theorem linear_independent.insert
modified theorem linear_independent.mono
modified theorem linear_independent.unique
modified def linear_independent
modified theorem linear_independent_empty
modified theorem linear_independent_iff
modified theorem linear_independent_span
modified theorem linear_independent_subtype
modified theorem linear_independent_union
modified theorem linear_independent_unique
modified theorem mem_span_insert_exchange
modified theorem module.card_fintype
modified def module_equiv_finsupp
modified theorem pi.is_basis_fun
modified theorem pi.is_basis_fun₀
modified theorem pi.is_basis_std_basis
modified theorem quotient_prod_linear_equiv
modified theorem span_le_span_iff
modified theorem vector_space.card_fintype
modified def alt_bilin_form.is_alt
modified theorem alt_bilin_form.neg
modified theorem alt_bilin_form.self_eq_zero
modified theorem bilin_form.add_left
modified theorem bilin_form.add_right
modified theorem bilin_form.ext
modified def bilin_form.is_ortho
modified theorem bilin_form.neg_left
modified theorem bilin_form.neg_right
modified theorem bilin_form.ortho_smul_left
modified theorem bilin_form.ortho_smul_right
modified theorem bilin_form.ortho_zero
modified theorem bilin_form.smul_left
modified theorem bilin_form.smul_right
modified theorem bilin_form.sub_left
modified theorem bilin_form.sub_right
modified theorem bilin_form.zero_left
modified theorem bilin_form.zero_right
modified structure bilin_form
modified def linear_map.to_bilin
modified theorem refl_bilin_form.eq_zero
modified theorem refl_bilin_form.ortho_sym
modified def sym_bilin_form.is_sym
modified theorem sym_bilin_form.ortho_sym
modified theorem sym_bilin_form.sym
modified theorem dim_add_le_dim_add_dim
modified theorem dim_bot
modified theorem dim_eq_injective
modified theorem dim_eq_surjective
modified theorem dim_fin_fun
modified theorem dim_fun'
modified theorem dim_fun
modified theorem dim_le_injective
modified theorem dim_le_of_submodule
modified theorem dim_le_surjective
modified theorem dim_map_le
modified theorem dim_of_field
modified theorem dim_pi
modified theorem dim_prod
modified theorem dim_quotient
modified theorem dim_range_add_dim_ker
modified theorem dim_range_le
modified theorem dim_range_of_surjective
modified theorem dim_span
modified theorem dim_span_le
modified theorem dim_span_of_finset
modified theorem dim_span_set
modified theorem dim_submodule_le
modified theorem dim_sup_add_dim_inf_eq
modified theorem dim_top
modified theorem exists_is_basis_fintype
modified theorem is_basis.le_span
modified theorem is_basis.mk_eq_dim
modified theorem is_basis.mk_range_eq_dim
modified theorem linear_equiv.dim_eq
modified theorem linear_equiv.dim_eq_lift
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_finset_sum_le
modified theorem rank_le_domain
modified theorem rank_le_range
modified theorem rank_zero
modified theorem direct_sum.component.of
modified def direct_sum.component
modified theorem direct_sum.ext
modified theorem direct_sum.ext_iff
modified def direct_sum.lmk
modified def direct_sum.lof
modified theorem direct_sum.lof_apply
modified theorem direct_sum.mk_smul
modified theorem direct_sum.of_smul
modified theorem direct_sum.single_eq_lof
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 theorem finsupp.ker_lsingle
modified def finsupp.lapply
modified theorem finsupp.lapply_apply
modified def finsupp.lmap_domain
modified theorem finsupp.lmap_domain_apply
modified theorem finsupp.lmap_domain_id
modified theorem finsupp.lmap_domain_total
modified def finsupp.lsingle
modified theorem finsupp.lsingle_apply
modified def finsupp.lsum
modified theorem finsupp.lsum_apply
modified theorem finsupp.mem_span_iff_total
modified theorem finsupp.mem_supported'
modified theorem finsupp.mem_supported
modified theorem finsupp.range_total
modified def finsupp.restrict_dom
modified theorem finsupp.restrict_dom_apply
modified theorem finsupp.span_single_image
modified def finsupp.supported
modified theorem finsupp.supported_empty
modified theorem finsupp.supported_univ
modified theorem finsupp.supr_lsingle_range
modified theorem finsupp.total_apply
modified theorem finsupp.total_emb_domain
modified theorem finsupp.total_map_domain
modified theorem finsupp.total_on_range
modified theorem finsupp.total_range
modified theorem finsupp.total_single
modified theorem eq_bot_iff_dim_eq_zero
modified def equiv_of_dim_eq_dim
modified theorem finsupp.dim_eq
modified theorem finsupp.is_basis_single
modified theorem injective_of_surjective
modified def lin_equiv_matrix'
modified def lin_equiv_matrix
modified def linear_map.to_matrix
modified theorem matrix.diagonal_to_lin
modified def matrix.eval
modified theorem matrix.ker_diagonal_to_lin
modified theorem matrix.mul_to_lin
modified theorem matrix.proj_diagonal
modified theorem matrix.range_diagonal
modified theorem matrix.rank_diagonal
modified theorem matrix.rank_vec_mul_vec
modified def matrix.to_lin
modified theorem matrix.to_lin_add
modified theorem matrix.to_lin_apply
modified theorem matrix.to_lin_zero
modified theorem to_lin_to_matrix
modified theorem to_matrix_to_lin
modified def alt_sesq_form.is_alt
modified theorem alt_sesq_form.neg
modified theorem alt_sesq_form.self_eq_zero
modified theorem refl_sesq_form.eq_zero
modified theorem refl_sesq_form.ortho_sym
modified theorem sesq_form.add_left
modified theorem sesq_form.add_right
modified theorem sesq_form.ext
modified def sesq_form.is_ortho
modified theorem sesq_form.neg_left
modified theorem sesq_form.neg_right
modified theorem sesq_form.ortho_smul_left
modified theorem sesq_form.ortho_smul_right
modified theorem sesq_form.ortho_zero
modified theorem sesq_form.smul_left
modified theorem sesq_form.smul_right
modified theorem sesq_form.sub_left
modified theorem sesq_form.sub_right
modified theorem sesq_form.zero_left
modified theorem sesq_form.zero_right
modified structure sesq_form
modified theorem sym_sesq_form.is_refl
modified def sym_sesq_form.is_sym
modified theorem sym_sesq_form.ortho_sym
modified theorem sym_sesq_form.sym