ext — Mathlib

English

The negation of a homogeneous localization degree component is defined componentwise.

Русский

Отрицание компонента степени в однородной локализации определяется компонентно.

LaTeX

$$$$ (-c).deg = c.deg \text{ and } (-c).num = -c.num, \; (-c).den = c.den. $$$$

Lean4

@[ext]
theorem ext {c1 c2 : NumDenSameDeg 𝒜 x} (hdeg : c1.deg = c2.deg) (hnum : (c1.num : A) = c2.num)
    (hden : (c1.den : A) = c2.den) : c1 = c2 :=
  by
  rcases c1 with ⟨i1, ⟨n1, hn1⟩, ⟨d1, hd1⟩, h1⟩
  rcases c2 with ⟨i2, ⟨n2, hn2⟩, ⟨d2, hd2⟩, h2⟩
  dsimp only [Subtype.coe_mk] at *
  subst hdeg hnum hden
  congr

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