fst_zmod_cast — Mathlib

English

For any a in ZMod n, the first projection of its cast to R × S equals the cast: (cast a : R × S).fst = cast a.

Русский

Для любого a ∈ ZMod n, первая компонента приведения в R × S совпадает с привидением: (cast a : R × S).fst = cast a.

LaTeX

$$$ (\operatorname{cast} a : R \times S).\mathrm{fst} = \operatorname{cast} a $$$

Lean4

@[simp]
theorem _root_.Prod.fst_zmod_cast (a : ZMod n) : (cast a : R × S).fst = cast a :=
  by
  cases n
  · rfl
  · simp [ZMod.cast]

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