`BookProof.ChapterFreeFieldBornSignOrientationCard.natCard_orientationPreserving_flip` (n : ℕ) : Nat.card {b : Fin (n + 1) → Bool // flipMatrix b ∈ Matrix.specialOrthogonalGroup (F

Proved

BookProof.ChapterFreeFieldBornSignOrientationCard.natCard_orientationPreserving_flip

by leonardopedro · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterFreeFieldBornSignOrientationCard.

BookProof.ChapterFreeFieldBornSignOrientationCard.natCard_orientationPreserving_flip (n : ℕ) : Nat.card {b : Fin (n + 1) → Bool // flipMatrix b ∈ Matrix.specialOrthogonalGroup (Fin (n + 1)) ℝ} = 2 ^ n

Formalization note: Lean 4 identifier BookProof.ChapterFreeFieldBornSignOrientationCard.natCard_orientationPreserving_flip.

Preamble

-- Generated from ChapterFreeFieldBornSignOrientationCard.lean — theorem BookProof.ChapterFreeFieldBornSignOrientationCard.natCard_orientationPreserving_flip
import Definitions.Def_ChapterFreeFieldBornSignHom
import Definitions.Def_ChapterFreeFieldBornSignMatrix
import Definitions.Def_ChapterFreeFieldBornSignOrientation
import Mathlib
import Definitions.Def_ChapterFreeFieldBornSignOrientationCard
open BookProof.ChapterFreeFieldBornSignOrientationCard


open BookProof.ChapterFreeFieldBornSignHom
open BookProof.ChapterFreeFieldBornSignMatrix
open BookProof.ChapterFreeFieldBornSignOrientation

Formal statement

theorem BookProof.ChapterFreeFieldBornSignOrientationCard.natCard_orientationPreserving_flip (n : ℕ) :
    Nat.card {b : Fin (n + 1) → Bool //
      flipMatrix b ∈ Matrix.specialOrthogonalGroup (Fin (n + 1)) ℝ} = 2 ^ n := by sorry

View graph