algEquivAevalXAddC_eq_iff — Mathlib

English

The map t ↦ φ_t = automorphism sending X to X + t is injective: if φ_t = φ_{t'}, then t = t'.

Русский

Отображение t ↦ φ_t, где X↦X+t, инъективно: если φ_t = φ_{t'}, то t = t'.

LaTeX

$$$\forall t,t' \in R,\; \operatorname{algEquivAevalXAddC}(t) = \operatorname{algEquivAevalXAddC}(t') \iff t = t'.$$$

Lean4

@[simp]
theorem algEquivAevalXAddC_eq_iff {R : Type*} [CommRing R] (t t' : R) :
    algEquivAevalXAddC t = algEquivAevalXAddC t' ↔ t = t' := by simp [algEquivAevalXAddC]

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