toBialgHom_inj — Mathlib

English

The injectivity of toBialgHom is asserted: if two bialg equivalences have the same underlying bialgHom, then they are equal.

Русский

Инъективность toBialgHom: если две биалгебровые эквивелентности имеют одинаковый базовый биалгоморфизм, то они равны.

LaTeX

$$$\\text{toBialgHom\_inj}: (e_1,e_2) \\text{ with } toBialgHom(e_1)=toBialgHom(e_2) \\Rightarrow e_1=e_2$$$

Lean4

@[simp, norm_cast]
theorem toBialgHom_inj {e₁ e₂ : A ≃ₐc[R] B} : (↑e₁ : A →ₐc[R] B) = e₂ ↔ e₁ = e₂ :=
  toBialgHom_injective.eq_iff

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