English
If P is a decidable proposition, then casting the piecewise expression (ite P m n) commutes with the cast, i.e., the cast of the piecewise equals the piecewise of the casts.
Русский
Если P решение, то приведение к α от разветвления (ite P m n) равняется разветвлению от приведения: ((ite P m n) : ℤ) cast = ite P (m cast) (n cast).
LaTeX
$$$ \forall {\alpha} [IntCast \alpha] (P : Prop) [Decidable P] (m n : \mathbb{Z}),\ ((\mathrm{ite}\ P\ m\ n : \mathbb{Z}) : \alpha) = \mathrm{ite}\ P (m : \alpha) (n : \alpha).$$$
Lean4
/-- `coe : ℤ → α` as a `RingHom`. -/
def castRingHom : ℤ →+* α where
toFun := Int.cast
map_zero' := cast_zero
map_add' := cast_add
map_one' := cast_one
map_mul' := cast_mul
