star'_quot — Mathlib

English

The star'-quotient respects taking stars on representatives: star' r hr ⟨Quot.mk _ a⟩ = ⟨Quot.mk _ (star a)⟩.

Русский

Звезда' на факторе сохраняет звездочки на представителях: star' r hr [a] = [star a].

LaTeX

$$$\\\\star' r hr \\\\langle Quot.mk \\\\_ a \\\\rangle = \\\\langle Quot.mk \\\\_ (star a) \\\\rangle.$$$

Lean4

theorem star'_quot (hr : ∀ a b, r a b → r (star a) (star b)) {a} :
    (star' r hr ⟨Quot.mk _ a⟩ : RingQuot r) = ⟨Quot.mk _ (star a)⟩ :=
  star'_def _ _ _

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