`BookProof.ChapterMackeyInducedSystem.inducedSystem_stabilizer_rep` (L : MulAction.stabilizer G x₀ →* (K ≃ₗᵢ[ℂ] K)) (s : X → G) (hs : ∀ x, s x • x₀ = x) (hs0 : s x₀ = 1) (a...

Proved

BookProof.ChapterMackeyInducedSystem.inducedSystem_stabilizer_rep

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterMackeyInducedSystem.

BookProof.ChapterMackeyInducedSystem.inducedSystem_stabilizer_rep (L : MulAction.stabilizer G x₀ →* (K ≃ₗᵢ[ℂ] K)) (s : X → G) (hs : ∀ x, s x • x₀ = x) (hs0 : s x₀ = 1) (a : MulAction.stabilizer G x₀) (f : FieldSpace X K) : ((inducedSystem L s hs).U (a : G) f) x₀ = L a (f x₀)

Formalization note: Lean 4 identifier BookProof.ChapterMackeyInducedSystem.inducedSystem_stabilizer_rep.

Preamble

-- Generated from ChapterMackeyInducedSystem.lean — theorem BookProof.ChapterMackeyInducedSystem.inducedSystem_stabilizer_rep
import Mathlib
import Definitions.Def_ChapterMackeyInducedSystem
import Definitions.Def_ChapterMackeyImprimitivity
open BookProof.ChapterMackeyImprimitivity
open BookProof.ChapterMackeyImprimitivity.ImprimitivitySystem
open BookProof.ChapterMackeyInducedSystem


open scoped InnerProductSpace
open Finset


open BookProof.ChapterMackeyImprimitivity

variable {G : Type*} [Group G] {X : Type*} [Fintype X] [DecidableEq X] [MulAction G X]
variable {K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
variable {x₀ : X}

variable {L : MulAction.stabilizer G x₀ →* (K ≃ₗᵢ[ℂ] K)} {s : X → G}
variable (L s)
variable {L s}
variable (X K) in

Formal statement

theorem BookProof.ChapterMackeyInducedSystem.inducedSystem_stabilizer_rep (L : MulAction.stabilizer G x₀ →* (K ≃ₗᵢ[ℂ] K)) (s : X → G)
    (hs : ∀ x, s x • x₀ = x) (hs0 : s x₀ = 1) (a : MulAction.stabilizer G x₀)
    (f : FieldSpace X K) :
    ((inducedSystem L s hs).U (a : G) f) x₀ = L a (f x₀) := by sorry

View graph