isUnitTrinomial_iff'' — Mathlib

English

A strengthened equivalence: if p and q satisfy p*p.mirror = q*q.mirror then p.IsUnitTrinomial iff q.IsUnitTrinomial.

Русский

Усиленная эквивалентность: если p*p.mirror = q*q.mirror, то p.IsUnitTrinomial эквивалентно q.IsUnitTrinomial.

LaTeX

$$$(p * p.mirror) = (q * q.mirror) \\Rightarrow (p.IsUnitTrinomial \\iff q.IsUnitTrinomial)$$$

Lean4

theorem isUnitTrinomial_iff'' (h : p * p.mirror = q * q.mirror) : p.IsUnitTrinomial ↔ q.IsUnitTrinomial := by
  rw [isUnitTrinomial_iff', isUnitTrinomial_iff', h]

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