isReduced_iff

Mathlib.Data.PNat.Xgcd

URI: https://scilib.ai/kg/mathlib#PNat.XgcdType.isReduced_iff

English

Two notions of reducedness are equivalent: IsReduced ⇔ IsReduced'.

Русский

Две концепции сокращенности эквивалентны: IsReduced ⇔ IsReduced'.

LaTeX

$$$u.IsReduced \\iff u.IsReduced'$$$

Lean4

theorem isReduced_iff : u.IsReduced ↔ u.IsReduced' :=
  succPNat_inj.symm

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

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

Разделы

Аффилиация

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