smul_div'

Mathlib.Algebra.Group.Action.Basic

URI: https://scilib.ai/kg/mathlib#smul_div'

English

Let M act on a group A. For all r ∈ M and x,y ∈ A, r • (x / y) = (r • x) / (r • y).

Русский

Пусть M действует на группу A. Тогда для всех r ∈ M и x,y ∈ A: r • (x / y) = (r • x) / (r • y).

LaTeX

$$$ \forall r \in M, x,y \in A,\ r \cdot (x / y) = (r \cdot x) / (r \cdot y). $$$

Lean4

theorem smul_div' (r : M) (x y : A) : r • (x / y) = r • x / r • y :=
  map_div (MulDistribMulAction.toMonoidHom A r) x y

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

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

Разделы

Аффилиация

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