mk_coe' — Mathlib

English

A refined constructor returns the inverse equivalence uniquely determined by the data.

Русский

Уточненный конструктор задаёт обратную эквивалентность уникальным образом по данным.

LaTeX

$$$ mk\_coe'(e,f,h_1,h_2,h_3,h_4,h_5) = e^{-1} $$$

Lean4

@[simp]
theorem mk_coe' (e : A₁ ≃ₐ[R] A₂) (f h₁ h₂ h₃ h₄ h₅) : (⟨⟨f, e, h₁, h₂⟩, h₃, h₄, h₅⟩ : A₂ ≃ₐ[R] A₁) = e.symm :=
  symm_bijective.injective <| ext fun _ => rfl

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