mul_one_sub

Mathlib.Algebra.Ring.Defs

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

English

Every Ring carries a natural NonUnitalRing structure by forgetting the unit.

Русский

Каждое кольцо обладает натуральной структурой неединичного кольца, забывая единичный элемент.

LaTeX

$$$Ring(\alpha) \to NonUnitalRing(\alpha)$$$

Lean4

theorem mul_one_sub (a b : α) : a * (1 - b) = a - a * b := by rw [mul_sub, mul_one]

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

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

Разделы

Аффилиация

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