Theorem: rot_state_vadd_vsub' (Instructor/Lectures/grad/case_study_symmetries.lean)

State before:
⊢ ∀ (g : Rotation) (p : State), g +ᵥ p -ᵥ p = g
Tactic:
_
State after:
no goals