Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 9ac6e8a

Browse files
committed
refactor(set_theory/pgame): rename pgame lemma (#3775)
Renamed `move_left_right_moves_neg_symm` to `move_left_left_moves_neg_symm` to make it consistent with the other 3 related lemmas
1 parent 658cd38 commit 9ac6e8a

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/set_theory/pgame.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -579,7 +579,7 @@ begin
579579
induction x,
580580
exact neg_neg.symm
581581
end
582-
@[simp] lemma move_left_right_moves_neg_symm {x : pgame} (i : right_moves x) :
582+
@[simp] lemma move_left_left_moves_neg_symm {x : pgame} (i : right_moves x) :
583583
move_left (-x) ((left_moves_neg x).symm i) = -(move_right x i) :=
584584
by { cases x, refl }
585585
@[simp] lemma move_left_right_moves_neg {x : pgame} (i : right_moves (-x)) :

0 commit comments

Comments
 (0)