constr_pow_algebraMap — Mathlib

English

There is a simple identity showing that constr applied to pb.gen equals y, i.e., pb.basis.constr A (\lambda i. y^i) pb.gen = y.

Русский

Существуют простые тождества: pb.basis.constr A (\lambda i. y^i) pb.gen = y.

LaTeX

$$$ pb.basis.constr A (\lambda i. y^{i}) pb.gen = y $$$

Lean4

theorem constr_pow_algebraMap (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0) (x : A) :
    pb.basis.constr A (fun i => y ^ (i : ℕ)) (algebraMap A S x) = algebraMap A S' x := by
  convert pb.constr_pow_aeval hy (C x) <;> rw [aeval_C]

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