ringEquiv_symm_apply — Mathlib

English

For a ring equivalence e, the inverse ring equivalence applied to b equals e.symm(b).

Русский

Для кольцевой эквивалентности e обратная эквивалентность применена к b равна e.symm(b).

LaTeX

$$$(\text{ringEquiv } e).\text{symm} (b) = e.symm(b)$$$

Lean4

theorem ringEquiv_symm_apply (e : α ≃ β) [Add β] [Mul β] (b : β) :
    by
    letI := Equiv.add e
    letI := Equiv.mul e
    exact (ringEquiv e).symm b = e.symm b :=
  rfl

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