Commit 2024-11-30 00:03 3d4e9f41

View on Github →

chore: change associativity of +ᵥ from infixl to infixr (#19321) Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Associativity.20rules.20for.20SMul.20and.20VAdd

Estimated changes

modified theorem Equiv.pointReflection_apply
modified theorem vadd_vsub
modified theorem vadd_vsub_assoc
modified theorem vadd_vsub_eq_sub_vsub
modified theorem vadd_vsub_vadd_cancel_left
modified theorem vadd_vsub_vadd_cancel_right
modified theorem vsub_vadd
modified theorem vsub_vadd_comm