proofZero

Mathlib.Tactic.FieldSimp

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

Lean4

/-- The empty field-simp-normal-form expression `[]` (representing `1` as an empty product of powers
of atoms) can be proved to be nonzero, strict positivity, etc., as needed, as specified by the
value of `DenomCondition`. -/
def proofZero {iM : Q(CommGroupWithZero $M)} : ∀ cond : DenomCondition (M := M) q(inferInstance), cond.proof []
  | .none => Unit.unit
  | .nonzero => q(one_ne_zero (α := $M))
  | .positive _ _ _ _ => q(zero_lt_one (α := $M))

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

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

Разделы

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

Аффилиация

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