sub_sq_comm

Mathlib.Algebra.Ring.Commute

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

English

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

Русский

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

LaTeX

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

Lean4

theorem sub_sq_comm (a b : R) : (a - b) ^ 2 = (b - a) ^ 2 := by rw [sub_sq', mul_right_comm, add_comm, sub_sq']

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

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

Разделы

Аффилиация

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