instHasNoLoopSymm

Mathlib.Algebra.Homology.HasNoLoop

URI: https://scilib.ai/kg/mathlib#ComplexShape.instHasNoLoopSymm

English

If a complex shape has NoLoop, then its symmetric shape also has NoLoop.

Русский

Если у формы без петли есть свойство, то симметричная форма имеет то же свойство.

LaTeX

$$$c.symm.HasanNoLoop \Rightarrow c.HasNoLoop$$

Lean4

instance : c.symm.HasNoLoop where not_rel_self j := c.not_rel_self j

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

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

Разделы

Аффилиация

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