starRingEnd_apply — Mathlib

English

For all x in R, starRingEnd(R)(x) = star x.

Русский

Для каждого x в R выполняется starRingEnd(R)(x) = star x.

LaTeX

$$$$ \operatorname{starRingEnd}(R)(x) = \star x. $$$$

Lean4

/-- This is not a simp lemma, since we usually want simp to keep `starRingEnd` bundled.
For example, for complex conjugation, we don't want simp to turn `conj x`
into the bare function `star x` automatically since most lemmas are about `conj x`. -/
theorem starRingEnd_apply (x : R) : starRingEnd R x = star x :=
  rfl

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