Theorems · Definition · group theory

QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom

{ι : Type u_1} →
  (A : ι → Type u_2) →
    [inst : (i : ι) → AddCommGroup (A i)] →
      (n : ℕ) → ((i : ι) → A i) ⧸ (nsmulAddMonoidHom n).range ≃+ ((i : ι) → A i ⧸ (nsmulAddMonoidHom n).range)

The isomorphism between the quotient of a product by the image of the multiplication-by-n map and the product of the quotients by the images of the multiplication-by-n maps on the factors.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroup