toSubring_one — Mathlib

English

The toSubring of the constant polynomial 1 is the constant polynomial 1.

Русский

toSubring константы 1 равен константе 1.

LaTeX

$$$\\text{toSubring}(1) = 1$$$

Lean4

@[simp]
theorem toSubring_one :
    toSubring (1 : R[X]) T (Set.Subset.trans coeffs_one <| Finset.singleton_subset_set_iff.2 T.one_mem) = 1 :=
  ext fun i =>
    Subtype.eq <| by
      rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero, OneMemClass.coe_one]

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