coe_aeval_mk_apply — Mathlib

English

For a subalgebra S ≤ A and x ∈ S, (aeval (⟨x, h⟩ : S) p) = aeval x p.

Русский

Для подалгебры S ⊆ A и x ∈ S, равенство выполняется: aeval(⟨x,h⟩) p = aeval x p.

LaTeX

$$$\forall S \le A,\; x \in S:\; (\operatorname{aeval}(\langle x, h\rangle) p : A) = \operatorname{aeval}(x) p.$$$

Lean4

@[simp]
theorem coe_aeval_mk_apply {S : Subalgebra R A} (h : x ∈ S) : (aeval (⟨x, h⟩ : S) p : A) = aeval x p :=
  (aeval_algHom_apply S.val (⟨x, h⟩ : S) p).symm

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