dvd_apply

Mathlib.Algebra.Ring.Divisibility.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.dvd_apply

English

For left-cancelative semigroups, Equiv.dvd g a = g*a.

Русский

Для левоотменяемых полугрупп Equiv.dvd g a = g*a.

LaTeX

$$$Equiv.dvd(g,a) = g \cdot a$$$

Lean4

@[simp]
theorem dvd_apply {G : Type*} [LeftCancelSemigroup G] (g a : G) : Equiv.dvd g a = g * a :=
  rfl

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

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

Разделы

Аффилиация

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