Commit 2023-06-29 05:08 a0f98218

View on Github →

feat: add lemmas about Equiv.pointReflection (#5568)

Estimated changes

Modified Mathlib/Algebra/AddTorsor.lean

added theorem Equiv.left_vsub_pointReflection

added theorem Equiv.pointReflection_vsub_left

added theorem Equiv.pointReflection_vsub_right

added theorem Equiv.right_vsub_pointReflection

Modified Mathlib/Analysis/NormedSpace/AddTorsor.lean

added theorem dist_left_pointReflection

added theorem dist_pointReflection_left

added theorem dist_pointReflection_right

added theorem dist_right_pointReflection

Modified Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean

added theorem midpoint_pointReflection_left

added theorem midpoint_pointReflection_right