mirror_eq_zero — Mathlib

English

For polynomials p over a semiring R, the mirror of p is zero if and only if p itself is zero.

Русский

Для полиномов p над полускольпом R зеркалирование полинома равно нулю тогда и только тогда, когда сам полином равен нулю.

LaTeX

$$$ p^{\\sim} = 0 \\iff p = 0 $$$

Lean4

@[simp]
theorem mirror_eq_zero : p.mirror = 0 ↔ p = 0 :=
  ⟨fun h => by rw [← p.mirror_mirror, h, mirror_zero], fun h => by rw [h, mirror_zero]⟩

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