sub_int_iff

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

URI: https://scilib.ai/kg/mathlib#LiouvilleWith.sub_int_iff

English

Same as above; a redundant entry mirroring sub_int_iff with simp attribute.

Русский

То же самое; дубликат с пометкой simp.

LaTeX

$$@[simp] theorem sub_int_iff : LiouvilleWith p (x - m) ↔ LiouvilleWith p x$$

Lean4

@[simp]
theorem sub_int_iff : LiouvilleWith p (x - m) ↔ LiouvilleWith p x := by rw [← Rat.cast_intCast, sub_rat_iff]

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

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

Разделы

Аффилиация

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