proof

Mathlib.Tactic.FieldSimp

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

Lean4

/-- Given a field-simp-normal-form expression `L` (a product of powers of atoms), a proof (according
to the value of `DenomCondition`) of that expression's nonzeroness, strict positivity, etc. -/
def proof {iM : Q(GroupWithZero $M)} (L : qNF M) : DenomCondition iM → Type
  | .none => Unit
  | .nonzero => Q(NF.eval $(qNF.toNF L) ≠ 0)
  | .positive _ _ _ _ => Q(0 < NF.eval $(qNF.toNF L))

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

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

Разделы

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

Аффилиация

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