intCast_eq

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.intCast_eq

English

The integer cast equality holds: z1.cast = z2.cast iff z1 = z2.

Русский

Равенство приведения к целому: z1.cast = z2.cast тогда и только тогда, когда z1 = z2.

LaTeX

$$$(z_1^{\text{cast}} = z_2^{\text{cast}}) \iff z_1 = z_2$$$

Lean4

@[norm_cast]
theorem intCast_eq (z1 z2 : ℤ) : (z1 : ℤ_[p]) = z2 ↔ z1 = z2 := by simp

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

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

Разделы

Аффилиация

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