Commit 2024-01-21 02:48 7466efcf

View on Github →

chore(Algebra/AddTorsor): names with lower indices (#9616) Use variable names p₁, p₂ etc instead of p1, p2 etc.

Estimated changes

modified theorem eq_of_vsub_eq_zero
modified theorem eq_vadd_iff_vsub_eq
modified theorem neg_vsub_eq_vsub_rev
modified theorem vadd_right_cancel
modified theorem vadd_right_cancel_iff
modified theorem vadd_vsub_assoc
modified theorem vadd_vsub_vadd_cancel_left
modified theorem vsub_add_vsub_cancel
modified theorem vsub_eq_sub
modified theorem vsub_eq_zero_iff_eq
modified theorem vsub_left_cancel
modified theorem vsub_left_cancel_iff
modified theorem vsub_right_cancel
modified theorem vsub_right_cancel_iff
modified theorem vsub_sub_vsub_cancel_left
modified theorem vsub_sub_vsub_cancel_right
modified theorem vsub_vadd
modified theorem vsub_vadd_comm
modified theorem vsub_vadd_eq_vsub_sub