Commit 2023-03-07 07:27 78261225

View on Github →

chore(linear_algebra/affine_space/midpoint): factor out lemmas about char_zero (#18555) This removes the dependency on char_p in analysis.convex.segment and analysis.normed.group.add_torsor.

Estimated changes

Modified src/analysis/convex/between.lean

Modified src/analysis/convex/slope.lean

Modified src/analysis/normed_space/add_torsor.lean

Modified src/analysis/normed_space/affine_isometry.lean

Modified src/analysis/normed_space/mazur_ulam.lean

Modified src/linear_algebra/affine_space/midpoint.lean

deleted theorem homothety_inv_of_two

deleted theorem homothety_inv_two

deleted theorem homothety_one_half

deleted theorem line_map_inv_two

deleted theorem line_map_one_half

deleted theorem pi_midpoint_apply

Created src/linear_algebra/affine_space/midpoint_zero.lean

added theorem homothety_inv_of_two

added theorem homothety_inv_two

added theorem homothety_one_half

added theorem line_map_inv_two

added theorem line_map_one_half

added theorem pi_midpoint_apply

Modified src/linear_algebra/affine_space/ordered.lean