toEquiv_commutes — Mathlib

English

Let f be a ring isomorphism R ≃+* S. The underlying equivalence obtained from viewing f as an additive equivalence coincides with the underlying equivalence obtained from viewing f as a multiplicative equivalence.

Русский

Пусть f — изоморфизм колец между R и S. Получающаяся из нього базовая эквивалентность не зависит от того, рассматривали ли его как аддитивное или как мультипликативное изоморфное отображение.

LaTeX

$$$ (f : R \equiv+* S).toEquiv = (f : R \equiv* S).toEquiv $$$

Lean4

/-- The two paths coercion can take to an `Equiv` are equivalent -/
theorem toEquiv_commutes (f : R ≃+* S) : (f : R ≃+ S).toEquiv = (f : R ≃* S).toEquiv :=
  rfl

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