toAlgEquiv_injective — Mathlib

English

The map assigning to each continuous algebra equivalence its underlying algebra equivalence is injective.

Русский

Отображение, сопоставляющее непрерывному алгебраическому эквиваленту соответствующий алгебраический эквивалент, инъективно.

LaTeX

$$toAlgEquiv : (A ≃A[R] B) → A ≃ₐ[R] B is injective$$

Lean4

theorem toAlgEquiv_injective : Function.Injective (toAlgEquiv : (A ≃A[R] B) → A ≃ₐ[R] B) :=
  by
  rintro ⟨e, _, _⟩ ⟨e', _, _⟩ rfl
  rfl

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