val_intCast — Mathlib

English

Val preserves integer embedding: (n : HomogeneousLocalization 𝒜 x).val = n for all integers n.

Русский

Val сохраняет вложение целых чисел: (n : HomogeneousLocalization 𝒜 x).val = n для всех целых n.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\; (n : \\mathrm{HomogeneousLocalization}(\\mathcal{A},x)).\\mathrm{val} = n$$$

Lean4

@[simp]
theorem val_intCast (n : ℤ) : (n : HomogeneousLocalization 𝒜 x).val = n :=
  show val (Int.castDef n) = _ by cases n <;> simp [Int.castDef, *]

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