Documentation

Mathlib.Data.ZMod.Quotient

ZMod n and quotient groups / rings #

This file relates ZMod n to the quotient group ℤ / AddSubgroup.zmultiples (n : ℤ) and to the quotient ring ℤ ⧸ Ideal.span {(n : ℤ)}.

Main definitions #

Tags #

zmod, quotient group, quotient ring, ideal quotient

modulo multiples of a : ℤ is ZMod a.natAbs.

Equations
Instances For

    modulo the ideal generated by n : ℕ is ZMod n.

    Equations
    Instances For

      modulo the ideal generated by a : ℤ is ZMod a.natAbs.

      Equations
      Instances For
        def ZMod.prodEquivPi {ι : Type u_3} [Fintype ι] (a : ι) (coprime : Pairwise fun (i j : ι) => (a i).Coprime (a j)) :
        ZMod (i : ι, a i) ≃+* ((i : ι) → ZMod (a i))

        The Chinese remainder theorem, elementary version for ZMod. See also Mathlib.Data.ZMod.Basic for versions involving only two numbers.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def AddAction.zmultiplesQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) :

          The quotient (ℤ ∙ a) ⧸ (stabilizer b) is cyclic of order minimalPeriod (a +ᵥ ·) b.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (n : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
            (AddAction.zmultiplesQuotientStabilizerEquiv a b).symm n = n.cast a,
            noncomputable def MulAction.zpowersQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) :

            The quotient (a ^ ℤ) ⧸ (stabilizer b) is cyclic of order minimalPeriod ((•) a) b.

            Equations
            Instances For
              theorem MulAction.zpowersQuotientStabilizerEquiv_symm_apply {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (n : ZMod (Function.minimalPeriod (fun (x : β) => a x) b)) :
              (MulAction.zpowersQuotientStabilizerEquiv a b).symm n = a, ^ n.cast
              noncomputable def MulAction.orbitZPowersEquiv {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) :
              (MulAction.orbit ((Subgroup.zpowers a)) b) ZMod (Function.minimalPeriod (fun (x : β) => a x) b)

              The orbit (a ^ ℤ) • b is a cycle of order minimalPeriod ((•) a) b.

              Equations
              Instances For
                noncomputable def AddAction.orbitZMultiplesEquiv {α : Type u_5} {β : Type u_6} [AddGroup α] (a : α) [AddAction α β] (b : β) :
                (AddAction.orbit ((AddSubgroup.zmultiples a)) b) ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)

                The orbit (ℤ • a) +ᵥ b is a cycle of order minimalPeriod (a +ᵥ ·) b.

                Equations
                Instances For
                  theorem AddAction.orbitZMultiplesEquiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
                  (AddAction.orbitZMultiplesEquiv a b).symm k = k.cast a, +ᵥ b,
                  theorem MulAction.orbitZPowersEquiv_symm_apply {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a x) b)) :
                  (MulAction.orbitZPowersEquiv a b).symm k = a, ^ k.cast b,
                  @[deprecated AddAction.orbitZMultiplesEquiv_symm_apply]
                  theorem AddAction.orbit_zmultiples_equiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
                  (AddAction.orbitZMultiplesEquiv a b).symm k = k.cast a, +ᵥ b,

                  Alias of AddAction.orbitZMultiplesEquiv_symm_apply.

                  theorem MulAction.orbitZPowersEquiv_symm_apply' {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (k : ) :
                  (MulAction.orbitZPowersEquiv a b).symm k = a, ^ k b,
                  theorem AddAction.orbitZMultiplesEquiv_symm_apply' {α : Type u_5} {β : Type u_6} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ) :
                  (AddAction.orbitZMultiplesEquiv a b).symm k = k a, +ᵥ b,
                  theorem AddAction.minimalPeriod_eq_card {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) [Fintype (AddAction.orbit ((AddSubgroup.zmultiples a)) b)] :
                  theorem MulAction.minimalPeriod_eq_card {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) [Fintype (MulAction.orbit ((Subgroup.zpowers a)) b)] :
                  instance AddAction.minimalPeriod_pos {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) [Finite (AddAction.orbit ((AddSubgroup.zmultiples a)) b)] :
                  NeZero (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)
                  Equations
                  • =
                  instance MulAction.minimalPeriod_pos {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) [Finite (MulAction.orbit ((Subgroup.zpowers a)) b)] :
                  NeZero (Function.minimalPeriod (fun (x : β) => a x) b)
                  Equations
                  • =
                  @[simp]
                  theorem Nat.card_zpowers {α : Type u_3} [Group α] (a : α) :

                  See also Fintype.card_zpowers.

                  @[simp]
                  theorem finite_zmultiples {α : Type u_3} [AddGroup α] {a : α} :
                  @[simp]
                  theorem finite_zpowers {α : Type u_3} [Group α] {a : α} :
                  @[simp]
                  theorem infinite_zmultiples {α : Type u_3} [AddGroup α] {a : α} :
                  @[simp]
                  theorem infinite_zpowers {α : Type u_3} [Group α] {a : α} :
                  ((Subgroup.zpowers a)).Infinite ¬IsOfFinOrder a
                  theorem IsOfFinOrder.finite_zpowers {α : Type u_3} [Group α] {a : α} :
                  IsOfFinOrder a((Subgroup.zpowers a)).Finite

                  Alias of the reverse direction of finite_zpowers.

                  theorem IsOfFinAddOrder.finite_zmultiples {α : Type u_3} [AddGroup α] {a : α} :