σ_smul — Mathlib

English

For any x in the base ring and y in the extension ring, the action of the image σ(x) on y equals the product x y in the extension ring.

Русский

Для любых x из базового кольца и y из расширенного кольца действие образа σ(x) на y равно произведению x y в расширенном кольце.

LaTeX

$$$P.\\sigma x \\cdot y = x \\cdot y$$$

Lean4

@[simp]
theorem σ_smul (x y) : P.σ x • y = x * y := by rw [Algebra.smul_def, algebraMap_σ]

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