Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-22 16:54 ea9cd029

View on Github →

refactor(geometry/euclidean/basic): adjust Euclidean geometry to use affine isometries for reflections (#8662)

Estimated changes

added theorem norm_sub_eq_norm_add
added def reflection
added theorem reflection_apply
added theorem reflection_involutive
added theorem reflection_reflection
added theorem reflection_symm