symm

Mathlib.NumberTheory.PythagoreanTriples

URI: https://scilib.ai/kg/mathlib#PythagoreanTriple.symm

English

If h is a Pythagorean triple x, y, z, then (y, x, z) is also a Pythagorean triple.

Русский

Если тройка h = (x, y, z) является Пифагоровой тройкой, то тройка (y, x, z) тоже такова.

LaTeX

$$$PythagoreanTriple x y z \Rightarrow PythagoreanTriple y x z$$$

Lean4

@[symm]
theorem symm (h : PythagoreanTriple x y z) : PythagoreanTriple y x z := by rwa [pythagoreanTriple_comm]

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

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

Разделы

Аффилиация

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