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 Mathlib/Algebra/AddTorsor.lean

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

Modified Mathlib/Algebra/Group/Action/Defs.lean

Modified Mathlib/Algebra/Group/Operations.lean

Modified Mathlib/Analysis/Normed/Affine/Isometry.lean

modified theorem AffineIsometryEquiv.pointReflection_apply

Modified Mathlib/Geometry/Euclidean/Basic.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

modified theorem AffineEquiv.pointReflection_apply

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean