DenomCondition

Mathlib.Tactic.FieldSimp

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.FieldSimp.DenomCondition

Lean4

/-- Constraints on denominators which may need to be considered in `field_simp`: no condition,
nonzeroness, or strict positivity. -/
inductive DenomCondition (iM : Q(GroupWithZero $M))
  | none
  | nonzero
  |
  positive (iM' : Q(PartialOrder $M)) (iM'' : Q(PosMulStrictMono $M)) (iM''' : Q(PosMulReflectLT $M))
    (iM'''' : Q(ZeroLEOneClass $M))

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

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

Разделы

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

Аффилиация

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