unop_list_prod — Mathlib

English

Let l be a list of elements of Mᵐᵒᵖ. The unop of the product equals the product of the unops in reverse order: l.prod.unop = (l.map unop).reverse.prod.

Русский

Пусть l – список элементов Mᵐᵒᵖ. Обратная операция удаляет противоположность: l.prod.unop = (l.map unop).reverse.prod.

LaTeX

$$$ (l.prod).\operatorname{unop} = (\mathrm{map}(\operatorname{unop})\,l).\mathrm{reverse}.prod $$$

Lean4

theorem unop_list_prod (l : List Mᵐᵒᵖ) : l.prod.unop = (l.map unop).reverse.prod := by
  rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse, op_comp_unop, map_id]

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