transfer_rw

Mathlib.Data.Num.ZNum

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

Lean4

/-- This tactic tries to turn an (in)equality about `ZNum`s to one about `Int`s by rewriting.
```lean
example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
  transfer_rw
  exact le_add_of_nonneg_right (mul_self_nonneg _)
```
-/
@[scoped tactic_parser 1000]
public meta def transfer_rw : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ZNum.transfer_rw 1024 (ParserDescr.nonReservedSymbol✝ "transfer_rw" false✝)

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

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

Разделы

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

Аффилиация

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