ofRingEquiv — Mathlib

English

Promotes a ring equivalence that respects scalar multiplication to an algebra equivalence.

Русский

Преобразует кольцевое эквивалентность, сохраняющую умножение на скаляры, в алгебраическое эквивалентное отображение.

LaTeX

$$$\\mathrm{ofRingEquiv} : (A_1 \\simeq_{R} A_2) $$$

Lean4

/-- Promotes a linear `RingEquiv` to an `AlgEquiv`. -/
@[simps apply symm_apply toEquiv]
def ofRingEquiv {f : A₁ ≃+* A₂} (hf : ∀ x, f (algebraMap R A₁ x) = algebraMap R A₂ x) : A₁ ≃ₐ[R] A₂ :=
  { f with
    toFun := f
    invFun := f.symm
    commutes' := hf }

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