algEquiv — Mathlib

English

There is a canonical algebra isomorphism from WithAbs v to R′; i.e., WithAbs v and R′ are algebraically identical over R.

Русский

Существует каноническое алгебраическое изоморфизм From WithAbs v к R′; то есть WithAbs v и R′ равны как алгебры над R.

LaTeX

$$$WithAbs\\,algEquiv\\,\\,(v) : (WithAbs\\,v)\\simeq_{R}\\,R'$$$

Lean4

/-- The canonical algebra isomorphism from an `R`-algebra `R'` with an absolute value `v`
to `R'`. -/
def algEquiv (v : AbsoluteValue R' S) : (WithAbs v) ≃ₐ[R] R' :=
  AlgEquiv.refl (A₁ := R')

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