Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-22 20:10 9945a162

View on Github →

refactor(analysis/normed_space/{add_torsor, mazur_ulam}): adjust Mazur-Ulam file to use affine isometries (#8661)

Estimated changes

Modified src/analysis/normed_space/add_torsor.lean

deleted theorem affine_map.continuous_linear_iff

deleted theorem isometric.coe_const_vadd

deleted theorem isometric.coe_const_vsub

deleted theorem isometric.coe_const_vsub_symm

deleted theorem isometric.coe_vadd_const

deleted theorem isometric.coe_vadd_const_symm

deleted def isometric.const_vadd

deleted theorem isometric.const_vadd_zero

deleted def isometric.const_vsub

deleted theorem isometric.dist_point_reflection_fixed

deleted theorem isometric.dist_point_reflection_self'

deleted theorem isometric.dist_point_reflection_self

deleted theorem isometric.dist_point_reflection_self_real

deleted def isometric.point_reflection

deleted theorem isometric.point_reflection_apply

deleted theorem isometric.point_reflection_fixed_iff

deleted theorem isometric.point_reflection_involutive

deleted theorem isometric.point_reflection_midpoint_left

deleted theorem isometric.point_reflection_midpoint_right

deleted theorem isometric.point_reflection_self

deleted theorem isometric.point_reflection_symm

deleted theorem isometric.point_reflection_to_equiv

deleted def isometric.vadd_const

deleted theorem isometric.vadd_const_to_equiv

deleted theorem isometry.vadd_vsub

Modified src/analysis/normed_space/affine_isometry.lean

added theorem affine_isometry_equiv.coe_const_vadd

added theorem affine_isometry_equiv.coe_const_vsub

added theorem affine_isometry_equiv.coe_vadd_const

added theorem affine_isometry_equiv.coe_vadd_const_symm

added def affine_isometry_equiv.const_vadd

added theorem affine_isometry_equiv.const_vadd_zero

added def affine_isometry_equiv.const_vsub

added theorem affine_isometry_equiv.dist_point_reflection_fixed

added theorem affine_isometry_equiv.dist_point_reflection_self'

added theorem affine_isometry_equiv.dist_point_reflection_self

added theorem affine_isometry_equiv.dist_point_reflection_self_real

added def affine_isometry_equiv.point_reflection

added theorem affine_isometry_equiv.point_reflection_apply

added theorem affine_isometry_equiv.point_reflection_fixed_iff

added theorem affine_isometry_equiv.point_reflection_involutive

added theorem affine_isometry_equiv.point_reflection_midpoint_left

added theorem affine_isometry_equiv.point_reflection_midpoint_right

added theorem affine_isometry_equiv.point_reflection_self

added theorem affine_isometry_equiv.point_reflection_symm

added theorem affine_isometry_equiv.point_reflection_to_affine_equiv

added theorem affine_isometry_equiv.symm_const_vsub

added def affine_isometry_equiv.vadd_const

added theorem affine_isometry_equiv.vadd_const_to_affine_equiv

added theorem affine_isometry_equiv.vadd_vsub

added theorem affine_map.continuous_linear_iff

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/normed_space/linear_isometry.lean

added theorem linear_isometry_equiv.coe_neg

added def linear_isometry_equiv.neg

added theorem linear_isometry_equiv.symm_neg

Modified src/analysis/normed_space/mazur_ulam.lean

added theorem isometric.coe_fn_to_real_affine_isometry_equiv

deleted theorem isometric.coe_to_affine_equiv

added theorem isometric.coe_to_real_affine_isometry_equiv

deleted def isometric.to_affine_equiv

added def isometric.to_real_affine_isometry_equiv