OAI/GroupTheory/FiniteLattice/CommonCoreStatement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteLattice.CommonCore.Statement line 12

   Source documentation

   Compatible extensions whose relative cores retain the inner automorphisms have a unique common extension, and the common core retains the inner automorphisms.

   def Statement (ι : Type*) [Finite ι] [Nonempty ι]
       (A : Subgroup K) (U : ι → Subgroup K) (hAU : ∀ i, A ≤ U i)
       (alpha : A →* MulAut T) (beta : ∀ i, U i →* MulAut T) : Prop :=
   …