red_invRev_iff

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.red_invRev_iff

← MathLib Explorer

English

Red (invRev L1) (invRev L2) is equivalent to Red L1 L2.

Русский

Red (invRev L1) (invRev L2) эквивалентно Red L1 L2.

LaTeX

$$$Red\\,(invRev\\ L_1)\\,(invRev\\ L_2)\\;\\iff\\; Red\\ L_1\\ L_2$$$

Lean4

@[to_additive (attr := simp)]
theorem red_invRev_iff : Red (invRev L₁) (invRev L₂) ↔ Red L₁ L₂ :=
  ⟨fun h => by simpa only [invRev_invRev] using h.invRev, fun h => h.invRev⟩

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

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

Разделы

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

Аффилиация

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