ofMul_div

Mathlib.Algebra.Group.TypeTags.Basic

URI: https://scilib.ai/kg/mathlib#ofMul_div

English

Division in α corresponds to subtraction of additive images: ofMul (x / y) = ofMul x − ofMul y.

Русский

Деление в α соответствует вычитанию образов в аддитивной копии: ofMul (x / y) = ofMul x − ofMul y.

LaTeX

$$ofMul(x / y) = ofMul x - ofMul y$$

Lean4

@[simp]
theorem ofMul_div [Div α] (x y : α) : ofMul (x / y) = ofMul x - ofMul y :=
  rfl

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

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

Разделы

Аффилиация

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