star_val_eq — Mathlib

English

For any self-adjoint element x in the additive group with involution, the star of its underlying value equals the value itself.

Русский

Для самосопряжённого элемента x в аддитивной группе с инволютой звезда применима равенство star(х) = х.

LaTeX

$$$\forall x \in \mathrm{selfAdjoint}(R),\ star(x) = x$$$

Lean4

@[simp, norm_cast]
theorem star_val_eq {x : selfAdjoint R} : star (x : R) = x :=
  x.prop

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