exists_smul_eq

Mathlib.Algebra.Group.Action.Pretransitive

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

English

For any x,y in α and a structuring action by M, there exists m in M such that m•x = y.

Русский

Для любых x,y∈α существует m∈M с m•x = y.

LaTeX

$$$\\exists m : M, m \\cdot x = y$$$

Lean4

@[to_additive]
theorem exists_smul_eq (x y : α) : ∃ m : M, m • x = y :=
  IsPretransitive.exists_smul_eq x y

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

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

Разделы

Аффилиация

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