Commit 2023-11-13 16:05 aa0957f1

View on Github →

fix(Mathlib/Analysis/NormedSpace/AddTorsor): remove bad simp lemma (#8387) This didn't actually work with simp, as the RHS needs a 𝕜 that can't be guessed.

Estimated changes

modified theorem dist_pointReflection_right
modified theorem dist_right_pointReflection