toHopfAlgIso_refl — Mathlib

English

The HopfAlgIso associated to a reflexive BialgEquiv is the identity isomorphism.

Русский

Изометрия HopfAlg, соответствующая тождественному эквиваленту бинарной биалгебры, является тождественным изоморфизмом.

LaTeX

$$$$ toHopfAlgIso(\\text{BialgEquiv.refl } R X) = \\mathrm{Iso.refl} (\\mathrm{ HopfAlgCat.of } R X). $$$$

Lean4

@[simp]
theorem toHopfAlgIso_refl : toHopfAlgIso (BialgEquiv.refl R X) = .refl _ :=
  rfl

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