coe_one

Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

URI: https://scilib.ai/kg/mathlib#SubMulAction.coe_one

English

For any p : SubMulAction R M and any n ≠ 0, the underlying set of p^n equals the nth power of the underlying set: ↑(p^n) = (p)^n.

Русский

Для p: SubMulAction R M и любого n ≠ 0 выполняется: ↑(p^n) = (p)^n.

LaTeX

$$$\\forall p:\\,\\mathrm{SubMulAction}\\,R\\,M\\; (n:\\,\\mathbb{N}),\\ n \\neq 0 \\implies \\uparrow(p^{n}) = (p)^{n}.$$$

Lean4

theorem coe_one : ↑(1 : SubMulAction R M) = Set.range fun r : R => r • (1 : M) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru