ext_num_den_iff

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#NNRat.ext_num_den_iff

English

For NRat p and q, p = q iff p.num = q.num and p.den = q.den.

Русский

Для NRat p и q верно: p = q тогда и только тогда, когда p.num = q.num и p.den = q.den.

LaTeX

$$$ p = q \iff p.num = q.num \land p.den = q.den $$$

Lean4

theorem ext_num_den_iff : p = q ↔ p.num = q.num ∧ p.den = q.den :=
  ⟨by rintro rfl; exact ⟨rfl, rfl⟩, fun h ↦ ext_num_den h.1 h.2⟩

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

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

Разделы

Аффилиация

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