coe_ofBijective — Mathlib

English

Let f: A →⋆* B be a star-multiplicative bijection. Then the underlying function of the associated StarMulEquiv is exactly f; i.e., the coercion of StarMulEquiv.ofBijective f hf to A → B equals f.

Русский

Пусть f: A →⋆* B есть биективный звёздно-умножающий гомоморфизм. Тогда соответствующее отображение StarMulEquiv, полученное из f, имеет в основе именно f; т.е. приводящая к A → B карта равна f.

LaTeX

$$$\\displaystyle (\\operatorname{StarMulEquiv.ofBijective} \\\\! f \\\\! hf : A \\to B) = f$$$

Lean4

@[simp]
theorem coe_ofBijective {f : A →⋆* B} (hf : Function.Bijective f) : (StarMulEquiv.ofBijective f hf : A → B) = f :=
  rfl

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