`BookProof.ChapterFreeFieldBornSignFiber.signFlip_involutive` {s : Fin n → ℝ} (hs : ∀ k, s k = 1 ∨ s k = -1) (x : EuclideanSpace ℝ (Fin n)) : signFlip s (signFlip s x) = x

Initializing...

`BookProof.ChapterFreeFieldBornSignFiber.signFlip_involutive` {s : Fin n → ℝ} (hs : ∀ k, s k = 1 ∨ s k = -1) (x : EuclideanSpace ℝ (Fin n)) : signFlip s (signFlip s x) = x · Prove2Me