star — Mathlib

English

On RingQuot, the star operation on a representative class [a] is the class of star a: star([a]) = [star a].

Русский

На RingQuot операция звезды над классом представителя [a] равна классу star a: star([a]) = [star a].

LaTeX

$$$\\\\star([a]) = [\\\\star a].$$$

Lean4

theorem star (hr : ∀ a b, r a b → r (star a) (star b)) ⦃a b : R⦄ (h : Rel r a b) : Rel r (star a) (star b) := by
  induction h with
  | of h => exact Rel.of (hr _ _ h)
  | add_left _ h =>
    rw [star_add, star_add]
    exact Rel.add_left h
  | mul_left _ h =>
    rw [star_mul, star_mul]
    exact Rel.mul_right h
  | mul_right _ h =>
    rw [star_mul, star_mul]
    exact Rel.mul_left h

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