mul_self_sub_one

Mathlib.Algebra.Ring.Commute

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

← MathLib Explorer

English

In a commutative ring, a^2 − b^2 = (a + b)(a − b).

Русский

В коммутативном кольце выполняется a^2 − b^2 = (a + b)(a − b).

LaTeX

$$$ a^2 - b^2 = (a + b)(a - b) $$$

Lean4

theorem mul_self_sub_one [NonAssocRing R] (a : R) : a * a - 1 = (a + 1) * (a - 1) := by
  rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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