coe_ringEquiv — Mathlib

English

The underlying ring equivalence of RingInvo R acts identically on elements of R, i.e., (f : R ≃+* Rᵐᵒᵖ) a = f a.

Русский

В базовом кольце RingInvo R эквивалентность кольца действует на элементы R идентично: (f : R ≃+* Rᵐᵒᵖ) a = f a.

LaTeX

$$$ (f : R \simeq R^{\mathrm{op}})\; a = f(a) $$$

Lean4

@[norm_cast]
theorem coe_ringEquiv (f : RingInvo R) (a : R) : (f : R ≃+* Rᵐᵒᵖ) a = f a :=
  rfl

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