`BookProof.ChapterFreeFieldBornSignOrientationQuotient.orientationQuotientEquiv_mk` (n : ℕ) (b : Fin (n + 1) → Bool) : orientationQuotientEquiv n (QuotientAddGroup.mk b) = orientat

Proved

BookProof.ChapterFreeFieldBornSignOrientationQuotient.orientationQuotientEquiv_mk

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterFreeFieldBornSignOrientationQuotient.

BookProof.ChapterFreeFieldBornSignOrientationQuotient.orientationQuotientEquiv_mk (n : ℕ) (b : Fin (n + 1) → Bool) : orientationQuotientEquiv n (QuotientAddGroup.mk b) = orientationCharacter (n + 1) b

Formalization note: Lean 4 identifier BookProof.ChapterFreeFieldBornSignOrientationQuotient.orientationQuotientEquiv_mk.

Preamble

-- Generated from ChapterFreeFieldBornSignOrientationQuotient.lean — theorem BookProof.ChapterFreeFieldBornSignOrientationQuotient.orientationQuotientEquiv_mk
import Definitions.Def_ChapterFreeFieldBornSignHom
import Definitions.Def_ChapterFreeFieldBornSignOrientationSubgroup
import Mathlib
import Definitions.Def_ChapterFreeFieldBornSignOrientationQuotient
open BookProof.ChapterFreeFieldBornSignOrientationQuotient


open BookProof.ChapterFreeFieldBornSignHom
open BookProof.ChapterFreeFieldBornSignOrientationSubgroup

Formal statement

theorem BookProof.ChapterFreeFieldBornSignOrientationQuotient.orientationQuotientEquiv_mk (n : ℕ) (b : Fin (n + 1) → Bool) :
    orientationQuotientEquiv n (QuotientAddGroup.mk b) =
      orientationCharacter (n + 1) b := by sorry

View graph