coe_ofBijective — Mathlib

English

The underlying function of the promoted algebra equivalence equals the original algebra homomorphism.

Русский

Базовая функция продвинутой алгебраической эквивалентности совпадает с исходным алгебра-гомоморфизмом.

LaTeX

$$$ (\\mathrm{ofBijective}(f, hf) : A_1 \\to A_2) = f $$$

Lean4

@[simp]
theorem coe_ofBijective (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) : (ofBijective f hf : A₁ → A₂) = f :=
  rfl

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