Module

CoprimeProjection.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.GroupTheory.CoprimeProjection

1 declaration indexed from sourceView source ↗

Module documentation

Coprimality through a joint group embedding

The inertia group of a compositum embeds in the product of the inertia groups of the two factors. This file records the elementary consequence needed to propagate tameness to the compositum.

Imports1

Mathlib.GroupTheory.Coset.Card

Imported by2

theorem

card_coprime_of_prod_injective

L23 ↗

TameAbhyankar.SGA1.card_coprime_of_prod_injective

Documentation

If a finite group embeds in a product of two finite groups whose orders are both prime to p, then its order is prime to p.

Source context 2 commands

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

noncomputable section
namespace TameAbhyankar.SGA1

Lean source · statement

theorem card_coprime_of_prod_injective
    {G H J : Type*} [Group G] [Group H] [Group J]
    [Finite G] [Finite H] [Finite J]
    (toH : G →* H) (toJ : G →* J)
    (hinjective : Function.Injective (toH.prod toJ))
    (p : ℕ)
    (hH : Nat.Coprime (Nat.card H) p)
    (hJ : Nat.Coprime (Nat.card J) p) :
    Nat.Coprime (Nat.card G) p

Module documentation

Coprimality through a joint group embedding

Declarations

card_coprime_of_prod_injective