toRingEquiv_algEquiv — Mathlib

English

For an automorphism σ of A1 that is R-algebraic, the underlying ring equivalence given by the action equals σ itself when viewed as a RingEquiv. In short, the ring-level equivalence induced by σ coincides with the algebra automorphism.

Русский

Для автоморфизма σ алгебры A1, являющегося R-алгебрической, соответствующее кольцевое эквивалентное отображение, получаемое через действие, совпадает с σ как RingEquiv.

LaTeX

$$$\\text{MulSemiringAction.toRingEquiv} \\_ {\\} \\ A_1 \\ \\sigma = \\sigma.$$$

Lean4

@[simp]
theorem _root_.MulSemiringAction.toRingEquiv_algEquiv (σ : A₁ ≃ₐ[R] A₁) : MulSemiringAction.toRingEquiv _ A₁ σ = σ :=
  rfl

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