transfer

Mathlib.Data.Num.ZNum

URI: https://scilib.ai/kg/mathlib#ZNum.transfer

Lean4

/-- This tactic tries to prove (in)equalities about `ZNum`s by transferring them to the `Int` world and
then trying to call `simp`.
```lean
example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
  transfer
  exact mul_self_nonneg _
```
-/
@[scoped tactic_parser 1000]
public meta def transfer : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ZNum.transfer 1024 (ParserDescr.nonReservedSymbol✝ "transfer" false✝)

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

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

Разделы

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

Аффилиация

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