SymmCongruences

Mathlib.Tactic.CC.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.SymmCongruences

Lean4

/-- The symmetric variant of `Congruences`.

The `Name` identifies which relation the congruence is considered for.
Note that this only works for two-argument relations: `ModEq n` and `ModEq m` are considered the
same. -/
abbrev SymmCongruences :=
  Std.HashMap SymmCongruencesKey (List (Expr × Name))

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

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

Разделы

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

Аффилиация

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