embeddingsMatrix_apply — Mathlib

English

Each entry of the embeddings matrix is exactly the image of the basis element under the corresponding embedding.

Русский

Каждый элемент матрицы вложений равен изображению базисного элемента под соответствующим вложением.

LaTeX

$$$\\big( \\mathrm{embeddingsMatrix}\\!\$A\\!\\!,C\\!\\!,b\\!\$ \\big)_{i,\\sigma} = \\sigma(b_i)$$$

Lean4

@[simp]
theorem embeddingsMatrix_apply (b : κ → B) (i) (σ : B →ₐ[A] C) : embeddingsMatrix A C b i σ = σ (b i) :=
  rfl

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