Commit 2025-03-03 00:15 90458847

View on Github →

chore: split long file Mathlib.LinearAlgebra.AffineSpace.AffineSubspace (#22384)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Basic.lean

Modified Mathlib/Analysis/Normed/Affine/AddTorsor.lean

Modified Mathlib/Analysis/Normed/Group/AddTorsor.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Created Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

added theorem AffineEquiv.coe_ofEq_apply

added def AffineEquiv.ofEq

added theorem AffineEquiv.ofEq_rfl

added theorem AffineEquiv.ofEq_symm

added theorem AffineEquiv.span_eq_top_iff

added theorem AffineMap.lineMap_mem

added theorem AffineMap.lineMap_mem_affineSpan_pair

added theorem AffineMap.lineMap_rev_mem_affineSpan_pair

added theorem AffineMap.map_top_of_surjective

added theorem AffineMap.span_eq_top_of_surjective

added theorem AffineMap.vectorSpan_image_eq_submodule_map

added theorem AffineSubspace.Parallel.direction_eq

added theorem AffineSubspace.Parallel.refl

added theorem AffineSubspace.Parallel.symm

added theorem AffineSubspace.Parallel.trans

added theorem AffineSubspace.Parallel.vectorSpan_eq

added def AffineSubspace.Parallel

added theorem AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq

added theorem AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty

added theorem AffineSubspace.bot_parallel_iff_eq_bot

added theorem AffineSubspace.coe_affineSpan_singleton

added theorem AffineSubspace.coe_comap

added theorem AffineSubspace.coe_inclusion_apply

added theorem AffineSubspace.coe_map

added theorem AffineSubspace.coe_subtype

added theorem AffineSubspace.coe_vadd

added theorem AffineSubspace.coe_vsub

added def AffineSubspace.comap

added theorem AffineSubspace.comap_bot

added theorem AffineSubspace.comap_comap

added theorem AffineSubspace.comap_id

added theorem AffineSubspace.comap_inf

added theorem AffineSubspace.comap_mono

added theorem AffineSubspace.comap_span

added theorem AffineSubspace.comap_supr

added theorem AffineSubspace.comap_symm

added theorem AffineSubspace.comap_top

added theorem AffineSubspace.direction_affineSpan_insert

added theorem AffineSubspace.direction_lt_of_nonempty

added theorem AffineSubspace.direction_sup

added theorem AffineSubspace.eq_univ_of_subsingleton_span_eq_top

added theorem AffineSubspace.gc_map_comap

added def AffineSubspace.inclusion

added theorem AffineSubspace.inclusion_rfl

added theorem AffineSubspace.le_comap_map

added def AffineSubspace.map

added theorem AffineSubspace.map_bot

added theorem AffineSubspace.map_comap_le

added theorem AffineSubspace.map_direction

added theorem AffineSubspace.map_eq_bot_iff

added theorem AffineSubspace.map_iSup

added theorem AffineSubspace.map_id

added theorem AffineSubspace.map_le_iff_le_comap

added theorem AffineSubspace.map_map

added theorem AffineSubspace.map_span

added theorem AffineSubspace.map_sup

added theorem AffineSubspace.map_symm

added theorem AffineSubspace.mem_affineSpan_insert_iff

added theorem AffineSubspace.mem_affineSpan_singleton

added theorem AffineSubspace.mem_comap

added theorem AffineSubspace.mem_map

added theorem AffineSubspace.mem_map_iff_mem_of_injective

added theorem AffineSubspace.mem_map_of_mem

added theorem AffineSubspace.parallel_bot_iff_eq_bot

added theorem AffineSubspace.parallel_comm

added theorem AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot

added theorem AffineSubspace.preimage_coe_affineSpan_singleton

added theorem AffineSubspace.subsingleton_of_subsingleton_span_eq_top

added theorem AffineSubspace.subtype_apply

added theorem AffineSubspace.subtype_injective

added theorem AffineSubspace.subtype_linear

added def AffineSubspace.topEquiv

added theorem AffineSubspace.vsub_left_mem_direction_iff_mem

added theorem AffineSubspace.vsub_right_mem_direction_iff_mem

added theorem affineSpan_coe_preimage_eq_top

added theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top

added theorem mem_vectorSpan_pair

added theorem mem_vectorSpan_pair_rev

added theorem smul_vsub_rev_vadd_mem_affineSpan_pair

added theorem smul_vsub_vadd_mem_affineSpan_pair

added theorem vadd_left_mem_affineSpan_pair

added theorem vadd_right_mem_affineSpan_pair

added theorem vectorSpan_eq_span_vsub_finset_right_ne

added theorem vectorSpan_eq_span_vsub_set_left

added theorem vectorSpan_eq_span_vsub_set_left_ne

added theorem vectorSpan_eq_span_vsub_set_right

added theorem vectorSpan_eq_span_vsub_set_right_ne

added theorem vectorSpan_image_eq_span_vsub_set_left_ne

added theorem vectorSpan_image_eq_span_vsub_set_right_ne

added theorem vectorSpan_pair

added theorem vectorSpan_pair_rev

added theorem vectorSpan_range_eq_span_range_vsub_left

added theorem vectorSpan_range_eq_span_range_vsub_left_ne

added theorem vectorSpan_range_eq_span_range_vsub_right

added theorem vectorSpan_range_eq_span_range_vsub_right_ne

added theorem vectorSpan_vadd

Renamed Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean to Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

deleted theorem AffineEquiv.coe_ofEq_apply

deleted def AffineEquiv.ofEq

deleted theorem AffineEquiv.ofEq_rfl

deleted theorem AffineEquiv.ofEq_symm

deleted theorem AffineEquiv.span_eq_top_iff

deleted theorem AffineMap.lineMap_mem

deleted theorem AffineMap.lineMap_mem_affineSpan_pair

deleted theorem AffineMap.lineMap_rev_mem_affineSpan_pair

deleted theorem AffineMap.map_top_of_surjective

deleted theorem AffineMap.span_eq_top_of_surjective

deleted theorem AffineMap.vectorSpan_image_eq_submodule_map

deleted theorem AffineSubspace.Parallel.direction_eq

deleted theorem AffineSubspace.Parallel.refl

deleted theorem AffineSubspace.Parallel.symm

deleted theorem AffineSubspace.Parallel.trans

deleted theorem AffineSubspace.Parallel.vectorSpan_eq

deleted def AffineSubspace.Parallel

deleted theorem AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq

deleted theorem AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty

deleted theorem AffineSubspace.bot_parallel_iff_eq_bot

deleted theorem AffineSubspace.coe_affineSpan_singleton

deleted theorem AffineSubspace.coe_comap

deleted theorem AffineSubspace.coe_inclusion_apply

deleted theorem AffineSubspace.coe_map

deleted theorem AffineSubspace.coe_subtype

deleted theorem AffineSubspace.coe_vadd

deleted theorem AffineSubspace.coe_vsub

deleted def AffineSubspace.comap

deleted theorem AffineSubspace.comap_bot

deleted theorem AffineSubspace.comap_comap

deleted theorem AffineSubspace.comap_id

deleted theorem AffineSubspace.comap_inf

deleted theorem AffineSubspace.comap_mono

deleted theorem AffineSubspace.comap_span

deleted theorem AffineSubspace.comap_supr

deleted theorem AffineSubspace.comap_symm

deleted theorem AffineSubspace.comap_top

deleted theorem AffineSubspace.direction_affineSpan_insert

deleted theorem AffineSubspace.direction_lt_of_nonempty

deleted theorem AffineSubspace.direction_sup

deleted theorem AffineSubspace.eq_univ_of_subsingleton_span_eq_top

deleted theorem AffineSubspace.gc_map_comap

deleted def AffineSubspace.inclusion

deleted theorem AffineSubspace.inclusion_rfl

deleted theorem AffineSubspace.le_comap_map

deleted def AffineSubspace.map

deleted theorem AffineSubspace.map_bot

deleted theorem AffineSubspace.map_comap_le

deleted theorem AffineSubspace.map_direction

deleted theorem AffineSubspace.map_eq_bot_iff

deleted theorem AffineSubspace.map_iSup

deleted theorem AffineSubspace.map_id

deleted theorem AffineSubspace.map_le_iff_le_comap

deleted theorem AffineSubspace.map_map

deleted theorem AffineSubspace.map_span

deleted theorem AffineSubspace.map_sup

deleted theorem AffineSubspace.map_symm

deleted theorem AffineSubspace.mem_affineSpan_insert_iff

deleted theorem AffineSubspace.mem_affineSpan_singleton

deleted theorem AffineSubspace.mem_comap

deleted theorem AffineSubspace.mem_map

deleted theorem AffineSubspace.mem_map_iff_mem_of_injective

deleted theorem AffineSubspace.mem_map_of_mem

deleted theorem AffineSubspace.parallel_bot_iff_eq_bot

deleted theorem AffineSubspace.parallel_comm

deleted theorem AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot

deleted theorem AffineSubspace.preimage_coe_affineSpan_singleton

deleted theorem AffineSubspace.subsingleton_of_subsingleton_span_eq_top

deleted theorem AffineSubspace.subtype_apply

deleted theorem AffineSubspace.subtype_injective

deleted theorem AffineSubspace.subtype_linear

deleted def AffineSubspace.topEquiv

deleted theorem AffineSubspace.vsub_left_mem_direction_iff_mem

deleted theorem AffineSubspace.vsub_right_mem_direction_iff_mem

deleted theorem affineSpan_coe_preimage_eq_top

deleted theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top

deleted theorem mem_vectorSpan_pair

deleted theorem mem_vectorSpan_pair_rev

deleted theorem smul_vsub_rev_vadd_mem_affineSpan_pair

deleted theorem smul_vsub_vadd_mem_affineSpan_pair

deleted theorem vadd_left_mem_affineSpan_pair

deleted theorem vadd_right_mem_affineSpan_pair

deleted theorem vectorSpan_eq_span_vsub_finset_right_ne

deleted theorem vectorSpan_eq_span_vsub_set_left

deleted theorem vectorSpan_eq_span_vsub_set_left_ne

deleted theorem vectorSpan_eq_span_vsub_set_right

deleted theorem vectorSpan_eq_span_vsub_set_right_ne

deleted theorem vectorSpan_image_eq_span_vsub_set_left_ne

deleted theorem vectorSpan_image_eq_span_vsub_set_right_ne

deleted theorem vectorSpan_pair

deleted theorem vectorSpan_pair_rev

deleted theorem vectorSpan_range_eq_span_range_vsub_left

deleted theorem vectorSpan_range_eq_span_range_vsub_left_ne

deleted theorem vectorSpan_range_eq_span_range_vsub_right

deleted theorem vectorSpan_range_eq_span_range_vsub_right_ne

deleted theorem vectorSpan_vadd

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Renamed Mathlib/LinearAlgebra/AffineSpace/Basic.lean to Mathlib/LinearAlgebra/AffineSpace/Defs.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Restrict.lean

Modified scripts/noshake.json