intCast_comp_cast — Mathlib

English

The two-stage casting Int.cast ∘ ZMod.cast coincides with ZMod.cast.

Русский

Два способа приведения в кольцо через целые числа и через ZMod совпадают.

LaTeX

$$$\\\\forall {n : \\\\mathbb{N}} (R : Type*), \\\\[inst : Ring R], (Int.cast \\\\circ ZMod.cast) = ZMod.cast$$

Lean4

/-- The coercions are respectively `Int.cast`, `ZMod.cast`, and `ZMod.cast`. -/
@[simp]
theorem intCast_comp_cast : ((↑) : ℤ → R) ∘ (cast : ZMod n → ℤ) = cast :=
  by
  cases n
  · exact congr_arg (Int.cast ∘ ·) ZMod.cast_id'
  · ext
    simp [ZMod, ZMod.cast]

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