surjective_smul

Mathlib.Algebra.Group.Action.Pretransitive

URI: https://scilib.ai/kg/mathlib#MulAction.surjective_smul

English

For an IsPretransitive action, the map c ↦ c•x from M to α is surjective for every x.

Русский

Для предпереставимого действия отображение c↦c•x сюръективно для каждого x.

LaTeX

$$$\\text{IsPretransitive } M \\alpha \\Rightarrow \\operatorname{Surjective}(c \\mapsto c \\cdot x)$$$

Lean4

@[to_additive]
theorem surjective_smul (x : α) : Surjective fun c : M ↦ c • x :=
  exists_smul_eq M x

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

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

Разделы

Аффилиация

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