mk_coe — Mathlib

English

The canonical constructor for an AlgEquiv returns the same object up to the specified equivalence data.

Русский

Канонический конструктор AlgEquiv возвращает тот же объект с заданной эквивалентностью.

LaTeX

$$$\\langle\\text{e},\\text{e'},\\text{h}_1,\\text{h}_2,\\text{h}_3,\\text{h}_4,\\text{h}_5\\rangle = e$$$

Lean4

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

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