ringEquiv_symm_mk — Mathlib

English

The inverse of the ring equivalence sends the class ⟦g⟧ to the canonical embedding of g into the i-th component.

Русский

Обратное к кольцевой эквивалентности отображает класс ⟦g⟧ в каноническое вложение элемента g в i-ю компоненту.

LaTeX

$$$(\\mathrm{ringEquiv}(G,f')).\\mathrm{symm}(\\langle g \\rangle) = \\mathrm{of}\\;G\\;i\\;g.2.$$$

Lean4

theorem ringEquiv_symm_mk [Nonempty ι] {g} : (ringEquiv G f').symm ⟦g⟧ = of _ _ g.1 g.2 :=
  rfl

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