toUnder_inv_right_apply — Mathlib

English

For a morphism f: A ≃ₐ[R] B, the inverse right component applied to b ∈ B equals f.symm(b).

Русский

Для изоморфизма f: A ≃ₐ[R] B правая компонента обратного применимо к b ∈ B даёт f.symm(b).

LaTeX

$$$f.toUnder.inv.right(b) = f.symm(b)$$$

Lean4

@[simp]
theorem toUnder_inv_right_apply {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B)
    (b : B) : f.toUnder.inv.right b = f.symm b :=
  rfl

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