OAI/GroupTheory/FiniteLattice/CommonCore.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteLattice.CommonCore.common_core line 12

   Source documentation

   Compatible extensions with relative cores mapping over the inner automorphisms glue uniquely over their generated group, whose core has the same image property.

   theorem common_core (K T : Type*) [Group K] [Finite K] [Group T] [IsSimpleGroup T]
       (ι : Type*) [Finite ι] [Nonempty ι]
       (A : Subgroup K) (U : ι → Subgroup K) (hAU : ∀ i, A ≤ U i)
       (alpha : A →* MulAut T) (beta : ∀ i, U i →* MulAut T) :
       Statement K T ι A U hAU alpha beta := by
   …

   Mentions: OAI.FiniteLattice.CommonCore.Statement