algEquivOfAlgEquiv_symm — Mathlib

English

For a RingEquiv h: A ≃ B, the induced ring equivalence on fraction fields sends algebraMap to algebraMap via h.

Русский

Для RingEquiv h: A ≃ B индуцированное кольцевое эквивалентное отображение на полях дробей переводит algebraMap через h.

LaTeX

$$$(\text{ringEquivOfRingEquiv } h)(\operatorname{algebraMap} A K a) = \operatorname{algebraMap} B L (h a)$$$

Lean4

@[simp]
theorem algEquivOfAlgEquiv_symm : (algEquivOfAlgEquiv h : K ≃ₐ[R] L).symm = algEquivOfAlgEquiv h.symm :=
  rfl

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