NYLL
Module

SigmaMonotonicity.lean

Nyll.ProCGroups.FiniteGroups.SigmaMonotonicity
2 declarations indexed from sourceView source ↗

Module documentation

Inclusion of finite Sigma-group classes

Enlarging the permitted primes preserves the actual prime-divisor condition. No nonemptiness or primality assumption on the containing sets is needed.

Imports1
Imported by2

Declarations

theorem

mono

L21 ↗
ProCGroups.FiniteGroupClass.IsSigmaNumber.mono
Documentation

A Sigma-number remains admissible when the set of permitted primes grows.

Source context 2 commands

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

namespace ProCGroups.FiniteGroupClass
universe u
Lean source · statement
theorem IsSigmaNumber.mono {sigma tau : Set ℕ} {n : ℕ}
    (h : sigma ⊆ tau) (hn : IsSigmaNumber sigma n) :
    IsSigmaNumber tau n
theorem

sigmaGroup_mono

L28 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_mono
Documentation

Inclusion of sets of primes gives inclusion of the corresponding finite-group classes.

Source context 2 commands

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

namespace ProCGroups.FiniteGroupClass
universe u
Lean source · statement
theorem sigmaGroup_mono {sigma tau : Set ℕ} (h : sigma ⊆ tau)
    {G : Type u} [Group G] (hG : sigmaGroup sigma G) : sigmaGroup tau G

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.