coe_star — Mathlib

English

For any unit u in R, the star of u, when coerced to R, equals the star of u coerced to R.

Русский

Для любого элемента-обратимого u в R звезда его равна звезде этого элемента, при приведении к R.

LaTeX

$$$\iota(\star u) = \star(\iota(u))$, где $\iota$ — естественное включение из $U(R)$ в $R$.$$

Lean4

@[simp]
theorem coe_star (u : Rˣ) : ↑(star u) = (star ↑u : R) :=
  rfl

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