of_def — Mathlib

English

The ith canonical injection from A_i into the free product is defined as the map ι i.

Русский

i-й канонический инъекция из A_i в свободное произведение задана как отображение ι i.

LaTeX

$$$\iota(i) : A_i \to_{\mathrm{Alg}} \mathrm{FreeProduct}(R,A)$$$

Lean4

theorem of_def : eta_helper Eq✝ @of.{} @(delta% @definition✝) :=
  by
  intros
  delta of
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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