mulOption_symm — Mathlib

English

Left options of x*y correspond to left options of y*x with indices swapped, up to quotient equivalence.

Русский

Левые опции x·y соответствуют левым опциям y·x с перестановкой индексов, с учетом эквивалентности частных.

LaTeX

$$⟦mulOption\ x\ y\ i\ j⟧ = ⟦mulOption\ y\ x\ j\ i⟧$$

Lean4

/-- The left options of `x * y` agree with that of `y * x` up to equivalence. -/
theorem mulOption_symm (x y) {i j} : ⟦mulOption x y i j⟧ = (⟦mulOption y x j i⟧ : Game) :=
  by
  dsimp only [mulOption, quot_sub, quot_add]
  rw [add_comm]
  congr 1
  on_goal 1 => congr 1
  all_goals rw [quot_mul_comm]

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