algebraMapThms

Mathlib.Tactic.Module

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Module.algebraMapThms

Lean4

/-- Lemmas used to post-process the result of the `match_scalars` and `module` tactics by converting
the `algebraMap` operations which (which proliferate in the constructed scalar goals) to more
familiar forms: `ℕ`, `ℤ` and `ℚ` casts. -/
def algebraMapThms : Array Name :=
  #[``eq_natCast, ``eq_intCast, ``eq_ratCast]

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

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

Разделы

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

Аффилиация

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