toAntisymmetrization_ofAntisymmetrization

Mathlib.Order.Antisymmetrization

URI: https://scilib.ai/kg/mathlib#toAntisymmetrization_ofAntisymmetrization

← MathLib Explorer

English

(Same as above) The composed maps give the identity on Antisymmetrization representatives.

Русский

(То же самое) compositions yield identity on representatives.

LaTeX

$$$\operatorname{toAntisymmetrization}(r)(\operatorname{ofAntisymmetrization}(r)\ a) = a$$$

Lean4

@[simp]
theorem toAntisymmetrization_ofAntisymmetrization (a : Antisymmetrization α r) :
    toAntisymmetrization r (ofAntisymmetrization r a) = a :=
  Quotient.out_eq' _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru