optionEquivRight_X_none — Mathlib

English

Under the right equivalence, the variable X applied to None becomes the constant polynomial C(X).

Русский

При отображении справа переменная X, примененная к None, превращается в константный полином C(X).

LaTeX

$$$\\operatorname{optionEquivRight} R S_1\\; (X(\\text{None})) = C(\\text{Polynomial.X})$$$

Lean4

theorem optionEquivRight_X_none : optionEquivRight R S₁ (X none) = C Polynomial.X := by
  simp [optionEquivRight_apply, aeval_X]

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