Theorems · Definition · group theory

FiniteIndexNormalAddSubgroup.comap

{G : Type u_1} →
  [inst : AddGroup G] →
    {H : Type u_2} → [inst_1 : AddGroup H] → (G →+ H) → FiniteIndexNormalAddSubgroup H → FiniteIndexNormalAddSubgroup G

The preimage of a finite-index normal additive subgroup under an additive homomorphism.

Defined in: Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Cited by: 4 results in Mathlib
Foundations: Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddGroup AddGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

AddGroupstatement and proof · cited by 4,410
AddSubgroupproof · cited by 3,232
AddMonoidHomstatement and proof · cited by 3,230
AddSubgroup.comapproof · cited by 123
FiniteIndexNormalAddSubgroupstatement and proof · cited by 26
FiniteIndexNormalAddSubgroup.toAddSubgroupproof · cited by 15

Cited by5

Results whose statement or proof uses this declaration.

ProfiniteAddGrp.ProfiniteCompletion.preimageproof · cited by 1
FiniteIndexNormalAddSubgroup.comap_monostatement and proof · cited by 1
FiniteIndexNormalAddSubgroup.toAddSubgroup_comapstatement · cited by 0
FiniteIndexNormalAddSubgroup.comap_compstatement and proof · cited by 0
FiniteIndexNormalAddSubgroup.comap_idstatement and proof · cited by 0