Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-28 06:06 7807f3d3

View on Github →

chore(linear_algebra/affine_space/basic): split (#4767)

  • Split linear_algebra/affine_space/basic into two files: affine_map and affine_subspace.
  • Move notation affine_space to the bottom of algebra/add_torsor.

Estimated changes

added theorem affine_map.add_linear
added theorem affine_map.coe_add
added theorem affine_map.coe_comp
added theorem affine_map.coe_const
added theorem affine_map.coe_fst
added theorem affine_map.coe_id
added theorem affine_map.coe_mk'
added theorem affine_map.coe_mk
added theorem affine_map.coe_mul
added theorem affine_map.coe_one
added theorem affine_map.coe_smul
added theorem affine_map.coe_snd
added theorem affine_map.coe_zero
added def affine_map.comp
added theorem affine_map.comp_apply
added theorem affine_map.comp_assoc
added theorem affine_map.comp_id
added def affine_map.const
added theorem affine_map.decomp'
added theorem affine_map.decomp
added theorem affine_map.ext
added theorem affine_map.ext_iff
added def affine_map.fst
added theorem affine_map.fst_linear
added def affine_map.id
added theorem affine_map.id_apply
added theorem affine_map.id_comp
added theorem affine_map.id_linear
added theorem affine_map.map_vadd
added def affine_map.mk'
added theorem affine_map.mk'_linear
added def affine_map.snd
added theorem affine_map.snd_linear
added theorem affine_map.vadd_apply
added theorem affine_map.vsub_apply
added theorem affine_map.zero_linear
added structure affine_map
added def affine_span
added theorem affine_span_mono
added theorem affine_span_nonempty
added theorem affine_subspace.ext
added theorem affine_subspace.le_def
added theorem affine_subspace.lt_def
added theorem affine_subspace.mk'_eq
added structure affine_subspace
added theorem coe_affine_span
added theorem direction_affine_span
added theorem mem_affine_span
added theorem mem_span_points
added def span_points
added theorem span_points_nonempty
added theorem subset_affine_span
added theorem subset_span_points
added def vector_span
added theorem vector_span_def
added theorem vector_span_empty
added theorem vector_span_mono
added theorem vector_span_singleton
added theorem vsub_mem_vector_span
deleted theorem affine_map.add_linear
deleted theorem affine_map.apply_line_map
deleted theorem affine_map.coe_add
deleted theorem affine_map.coe_comp
deleted theorem affine_map.coe_const
deleted theorem affine_map.coe_fst
deleted theorem affine_map.coe_id
deleted theorem affine_map.coe_line_map
deleted theorem affine_map.coe_mk'
deleted theorem affine_map.coe_mk
deleted theorem affine_map.coe_mul
deleted theorem affine_map.coe_one
deleted theorem affine_map.coe_smul
deleted theorem affine_map.coe_snd
deleted theorem affine_map.coe_zero
deleted def affine_map.comp
deleted theorem affine_map.comp_apply
deleted theorem affine_map.comp_assoc
deleted theorem affine_map.comp_id
deleted theorem affine_map.comp_line_map
deleted def affine_map.const
deleted theorem affine_map.const_linear
deleted theorem affine_map.decomp'
deleted theorem affine_map.decomp
deleted theorem affine_map.ext
deleted theorem affine_map.ext_iff
deleted def affine_map.fst
deleted theorem affine_map.fst_line_map
deleted theorem affine_map.fst_linear
deleted theorem affine_map.homothety_add
deleted theorem affine_map.homothety_def
deleted theorem affine_map.homothety_mul
deleted theorem affine_map.homothety_one
deleted theorem affine_map.homothety_zero
deleted def affine_map.id
deleted theorem affine_map.id_apply
deleted theorem affine_map.id_comp
deleted theorem affine_map.id_linear
deleted theorem affine_map.image_interval
deleted def affine_map.line_map
deleted theorem affine_map.line_map_apply
deleted theorem affine_map.line_map_same
deleted theorem affine_map.line_map_symm
deleted theorem affine_map.map_vadd
deleted def affine_map.mk'
deleted theorem affine_map.mk'_linear
deleted def affine_map.snd
deleted theorem affine_map.snd_line_map
deleted theorem affine_map.snd_linear
deleted theorem affine_map.to_fun_eq_coe
deleted theorem affine_map.vadd_apply
deleted theorem affine_map.vsub_apply
deleted theorem affine_map.zero_linear
deleted structure affine_map
deleted def affine_span
deleted theorem affine_span_mono
deleted theorem affine_span_nonempty
deleted theorem affine_subspace.bot_coe
deleted theorem affine_subspace.ext
deleted theorem affine_subspace.inf_coe
deleted theorem affine_subspace.le_def'
deleted theorem affine_subspace.le_def
deleted theorem affine_subspace.lt_def
deleted theorem affine_subspace.mem_coe
deleted theorem affine_subspace.mem_top
deleted def affine_subspace.mk'
deleted theorem affine_subspace.mk'_eq
deleted theorem affine_subspace.span_univ
deleted theorem affine_subspace.top_coe
deleted structure affine_subspace
deleted theorem coe_affine_span
deleted theorem direction_affine_span
deleted theorem mem_affine_span
deleted theorem mem_span_points
deleted def span_points
deleted theorem span_points_nonempty
deleted theorem subset_affine_span
deleted theorem subset_span_points
deleted def vector_span
deleted theorem vector_span_def
deleted theorem vector_span_empty
deleted theorem vector_span_mono
deleted theorem vector_span_singleton
deleted theorem vsub_mem_vector_span