`BookProof.PermSector.tensor_triple_induction` {X Y Z : Type*} [AddCommGroup X] [Module ℂ X] [AddCommGroup Y] [Module ℂ Y] [AddCommGroup Z] [Module ℂ Z] {P : X ⊗[ℂ] (Y ⊗[ℂ] Z) → Pr

Proved

BookProof.PermSector.tensor_triple_induction

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterPermutationSectorEsa.

BookProof.PermSector.tensor_triple_induction {X Y Z : Type*} [AddCommGroup X] [Module ℂ X] [AddCommGroup Y] [Module ℂ Y] [AddCommGroup Z] [Module ℂ Z] {P : X ⊗[ℂ] (Y ⊗[ℂ] Z) → Prop} (hzero : P 0) (htmul : ∀ (x : X) (y : Y) (z : Z), P (x ⊗ₜ[ℂ] (y ⊗ₜ[ℂ] z))) (hadd : ∀ u v, P u → P v → P (u + v)) (t : X ⊗[ℂ] (Y ⊗[ℂ] Z)) : P t

Formalization note: Lean 4 identifier BookProof.PermSector.tensor_triple_induction.

Preamble

-- Generated from ChapterPermutationSectorEsa.lean — theorem BookProof.PermSector.tensor_triple_induction
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterGraphCoreTransfer
import Definitions.Def_ChapterReducingSubspaceEsa
import Definitions.Def_ChapterTensorGraphCore
import Definitions.Def_ChapterGroupAverageEsa
import Definitions.Def_ChapterTensorPermutation
import Mathlib
import Definitions.Def_ChapterPermutationSectorEsa
open BookProof.PermSector



open scoped TensorProduct
open BookProof.FarisLavine BookProof.GraphCore BookProof.ReducedEsa BookProof.TensorCore
open BookProof.GroupAverage BookProof.TensorPerm

noncomputable section

Formal statement

theorem BookProof.PermSector.tensor_triple_induction {X Y Z : Type*} [AddCommGroup X] [Module ℂ X]
    [AddCommGroup Y] [Module ℂ Y] [AddCommGroup Z] [Module ℂ Z]
    {P : X ⊗[ℂ] (Y ⊗[ℂ] Z) → Prop} (hzero : P 0)
    (htmul : ∀ (x : X) (y : Y) (z : Z), P (x ⊗ₜ[ℂ] (y ⊗ₜ[ℂ] z)))
    (hadd : ∀ u v, P u → P v → P (u + v)) (t : X ⊗[ℂ] (Y ⊗[ℂ] Z)) : P t := by sorry

View graph