ofBijective — Mathlib

English

Promotes a bijective BialgHom to a BialgEquiv.

Русский

Преобразование биективного BialgHom в BialgEquiv.

LaTeX

$$$\\text{ofBijective } f \\; hf : A \\simeq_{\\text{bialg}} B$$$

Lean4

/-- Promotes a bijective bialgebra homomorphism to a bialgebra equivalence. -/
@[simps! apply]
noncomputable def ofBijective (f : A →ₐc[R] B) (hf : Bijective f) : A ≃ₐc[R] B :=
  .ofAlgEquiv (.ofBijective (f : A →ₐ[R] B) hf) (by ext; simp) (by ext; simp)

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