comp_aeval — Mathlib

English

Let φ be an algebra homomorphism from S1 to B over R. Then composing φ with aeval_f equals aeval_{i ↦ φ(f(i))}.

Русский

Пусть φ — алгебра-гомоморфизм из S1 в B над R. Тогда композиция φ с aeval_f равна aeval_{i ↦ φ(f(i))}.

LaTeX

$$$$ \phi \circ \mathrm{aeval}_f = \mathrm{aeval}_{\, (i \mapsto \phi(f(i)))} $$$$

Lean4

theorem comp_aeval {B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) :
    φ.comp (aeval f) = aeval fun i => φ (f i) := by
  ext i
  simp

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