Commit 2023-06-30 17:15 f0b3edea

View on Github →

feat: add a file about perpendicular bisector (#5627)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/Euclidean/Basic.lean

deleted theorem EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq

Created Mathlib/Geometry/Euclidean/PerpBisector.lean

added theorem AffineSubspace.direction_perpBisector

added theorem AffineSubspace.left_mem_perpBisector

added theorem AffineSubspace.mem_perpBisector_iff_dist_eq'

added theorem AffineSubspace.mem_perpBisector_iff_dist_eq

added theorem AffineSubspace.mem_perpBisector_iff_inner_eq

added theorem AffineSubspace.mem_perpBisector_iff_inner_eq_inner

added theorem AffineSubspace.mem_perpBisector_iff_inner_eq_zero'

added theorem AffineSubspace.mem_perpBisector_iff_inner_eq_zero

added theorem AffineSubspace.mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero

added theorem AffineSubspace.mem_perpBisector_pointReflection_iff_inner_eq_zero

added theorem AffineSubspace.midpoint_mem_perpBisector

added def AffineSubspace.perpBisector

added theorem AffineSubspace.perpBisector_comm

added theorem AffineSubspace.perpBisector_eq_top

added theorem AffineSubspace.perpBisector_ne_bot

added theorem AffineSubspace.perpBisector_nonempty

added theorem AffineSubspace.perpBisector_self

added theorem AffineSubspace.right_mem_perpBisector

added theorem EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq

added theorem Isometry.mapsTo_perpBisector

added theorem Isometry.preimage_perpBisector