Module

Solvable.lean

Nyll.ProCGroups.FiniteGroups.Solvable

10 declarations indexed from sourceView source ↗

Module documentation

Closure properties of finite solvable groups

This module packages the standard subgroup, finite-product, extension, formation, and hereditary closure properties of FiniteGroupClass.solvable.

Imports1

Nyll.ProCGroups.FiniteGroups.StandardClasses

Imported by2

theorem

isSolvable_pi_of_fintype

L23 ↗

ProCGroups.FiniteGroupClass.isSolvable_pi_of_fintype

Documentation

A finite product of solvable groups is solvable.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem isSolvable_pi_of_fintype
    {ι : Type u} [Finite ι]
    {G : ι → Type u} [∀ i, Group (G i)]
    (hG : ∀ i, Group.IsSolvable (G i)) :
    Group.IsSolvable (∀ i, G i)

theorem

solvable_subgroupClosed

L47 ↗

ProCGroups.FiniteGroupClass.solvable_subgroupClosed

Documentation

Finite solvable groups are closed under subgroups.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem solvable_subgroupClosed : SubgroupClosed solvable

theorem

solvable_finiteProductClosed

L54 ↗

ProCGroups.FiniteGroupClass.solvable_finiteProductClosed

Documentation

Finite solvable groups are closed under finite direct products.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem solvable_finiteProductClosed : FiniteProductClosed solvable

theorem

solvable_variety

L61 ↗

ProCGroups.FiniteGroupClass.solvable_variety

Documentation

Finite solvable groups form a variety of finite groups.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem solvable_variety : Variety solvable

theorem

solvable_formation

L65 ↗

ProCGroups.FiniteGroupClass.solvable_formation

Documentation

Finite solvable groups form a formation.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem solvable_formation : Formation solvable

theorem

solvable_extensionClosed

L69 ↗

ProCGroups.FiniteGroupClass.solvable_extensionClosed

Documentation

Finite solvable groups are closed under extensions.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem solvable_extensionClosed : ExtensionClosed solvable

theorem

solvable_normalSubgroupClosed

L77 ↗

ProCGroups.FiniteGroupClass.solvable_normalSubgroupClosed

Documentation

Finite solvable groups are closed under normal subgroups.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem solvable_normalSubgroupClosed : NormalSubgroupClosed solvable

theorem

solvable_melnikovFormation

L82 ↗

ProCGroups.FiniteGroupClass.solvable_melnikovFormation

Documentation

Finite solvable groups form a Melnikov formation.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · full declaration

theorem solvable_melnikovFormation : MelnikovFormation solvable where
  formation := solvable_formation
  normalSubgroupClosed := solvable_normalSubgroupClosed
  extensionClosed := solvable_extensionClosed

theorem

solvable_fullFormation

L88 ↗

ProCGroups.FiniteGroupClass.solvable_fullFormation

Documentation

Finite solvable groups form a full formation.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · full declaration

theorem solvable_fullFormation : FullFormation solvable where
  melnikovFormation := solvable_melnikovFormation
  subgroupClosed := solvable_subgroupClosed

theorem

solvable_hereditary

L93 ↗

ProCGroups.FiniteGroupClass.solvable_hereditary

Documentation

Finite solvable groups form a hereditary finite-group class.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem solvable_hereditary : Hereditary solvable

Module documentation

Closure properties of finite solvable groups

Declarations