mk_coe — Mathlib

English

Constructing a StarAlgEquiv from components yields the original map when all pieces are substituted.

Русский

Построение ⋆-эквивалентности из компонентов даёт исходную функцию при подстановке всех частей.

LaTeX

$$$$ (\langle\langle\langle e, e', h_1, h_2\rangle, h_3, h_4\rangle, h_5, h_6\rangle : A \simeq_{\star}^{R} B) = e. $$$$

Lean4

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

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