Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-18 21:34 61e1111d

View on Github →

chore(linear_algebra/affine_space): introduce notation for affine_map (#4675)

Estimated changes

Modified src/analysis/convex/basic.lean

modified theorem concave_on.comp_affine_map

modified theorem convex.affine_image

modified theorem convex.affine_preimage

modified theorem convex.combo_affine_apply

modified theorem convex_on.comp_affine_map

Modified src/analysis/convex/extrema.lean

Modified src/analysis/normed_space/mazur_ulam.lean

modified def isometric.to_affine_map

Modified src/geometry/euclidean/basic.lean

modified def euclidean_geometry.orthogonal_projection

Modified src/linear_algebra/affine_space/basic.lean

modified theorem affine_map.add_linear

modified theorem affine_map.apply_line_map

modified theorem affine_map.coe_add

modified theorem affine_map.coe_comp

modified theorem affine_map.coe_fst

modified theorem affine_map.coe_mul

modified theorem affine_map.coe_one

modified theorem affine_map.coe_smul

modified theorem affine_map.coe_snd

modified theorem affine_map.coe_zero

modified def affine_map.comp

modified theorem affine_map.comp_apply

modified theorem affine_map.comp_assoc

modified theorem affine_map.comp_id

modified theorem affine_map.comp_line_map

modified def affine_map.const

modified theorem affine_map.decomp'

modified theorem affine_map.decomp

modified theorem affine_map.ext

modified theorem affine_map.ext_iff

modified def affine_map.fst

modified theorem affine_map.fst_linear

modified def affine_map.homothety

modified def affine_map.homothety_affine

modified def affine_map.homothety_hom

modified def affine_map.id

modified theorem affine_map.id_comp

modified theorem affine_map.image_interval

modified def affine_map.line_map

modified theorem affine_map.linear_map_vsub

modified theorem affine_map.map_vadd

modified def affine_map.snd

modified theorem affine_map.snd_linear

modified theorem affine_map.to_fun_eq_coe

modified theorem affine_map.vadd_apply

modified theorem affine_map.vsub_apply

modified theorem affine_map.zero_linear

modified def linear_map.to_affine_map

Modified src/linear_algebra/affine_space/combination.lean

modified def affine_map.weighted_vsub_of_point

modified def finset.affine_combination

Modified src/topology/algebra/affine.lean

modified theorem affine_map.continuous_iff