Theorems · Theorem · group theory

QuotientAddGroup.strictMono_comap_prod_image

∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α),
  StrictMono fun t => (AddSubgroup.comap s.subtype t, QuotientAddGroup.mk '' ↑t)

Given an additive subgroup s, the function that sends an additive subgroup t to the pair consisting of its intersection with s and its image in the quotient α ⧸ s is strictly monotone, even though it is not injective in general.

Defined in

Mathlib.GroupTheory.Coset.Basic

Cited by

1 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroup