isPGroup_multiplicative — Mathlib

English

Let G be an additive group with a Z/nZ-module structure; then the multiplicative group (Multiplicative G) is an n-group.

Русский

Пусть G — аддитивная группа с модулем над Z/nZ; тогда умножаемая группа (Multiplicative G) является n-группой.

LaTeX

$$$\text{IsPGroup } n (\text{Multiplicative } G).$$$

Lean4

theorem isPGroup_multiplicative : IsPGroup n (Multiplicative G) := by
  simpa [IsPGroup, Multiplicative.forall] using fun _ ↦ ⟨1, by simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]⟩

Похожие утверждения