star_ratCast — Mathlib

English

For a division ring with star, the star of any rational embedded into the ring equals the rational itself.

Русский

Для кольца делимости с звездой звезда над любым рациональным, встроенным в кольцо, равна самому рациональному.

LaTeX

$$$\\\\star(r) = r \\\\quad( r \\\\in \\\\mathbb{Q}).$$$

Lean4

@[simp, norm_cast]
theorem star_ratCast [DivisionRing R] [StarRing R] (r : ℚ) : star (r : R) = r :=
  (congr_arg unop <| map_ratCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) r).trans (unop_ratCast _)

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