ofBijective_apply — Mathlib

English

For a bijective star-multiplicative homomorphism f and any a ∈ A, StarMulEquiv.ofBijective f hf applied to a yields f a; i.e., the map is evaluated pointwise by f.

Русский

Для биективного звёздного умножающего гомоморфизма f и любого a ∈ A выполняется: StarMulEquiv.ofBijective f hf a = f a.

LaTeX

$$$\\displaystyle \\text{ofBijective_apply }\\{f : A \\to⋆* B\\} (hf) (a) :\\; StarMulEquiv.ofBijective f hf \\; a = f a$$$

Lean4

theorem ofBijective_apply {f : A →⋆* B} (hf : Function.Bijective f) (a : A) : StarMulEquiv.ofBijective f hf a = f a :=
  rfl

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