σ_injective — Mathlib

English

The map σ is injective; different generators map to different elements in P.Ring, ensuring faithful embedding of the generator set.

Русский

Отображение σ инъективно; разные генераторы имеют разные образы в P.Ring, обеспечивая точную вложенность набора генераторов.

LaTeX

$$P.σ.Injective$$

Lean4

theorem σ_injective : P.σ.Injective := by
  intro x y e
  rw [← P.aeval_val_σ x, ← P.aeval_val_σ y, e]

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