mirror_monomial — Mathlib

English

The mirror of a monomial is the monomial itself.

Русский

Зеркало монома равно собственно мономиалу.

LaTeX

$$$ (\mathrm{monomial}\ n\ a).mirror = \mathrm{monomial}\ n\ a $$$

Lean4

theorem mirror_monomial (n : ℕ) (a : R) : (monomial n a).mirror = monomial n a := by
  classical
  by_cases ha : a = 0
  · rw [ha, monomial_zero_right, mirror_zero]
  ·
    rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ← C_mul_X_pow_eq_monomial,
      reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero, mul_one]

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