a : ℤ
⊢ ↑χ₈' ↑a = ↑χ₄ ↑↑a * ↑χ₈ ↑a
a : ℤ
⊢ ↑χ₈' ↑a = ↑χ₄ ↑a * ↑χ₈ ↑a
rw [← @cast_int_cast 8 (ZMod 4) _ 4 _ (by norm_num) a]
no goals
a : ℤ
⊢ ↑χ₈' ↑a = ↑χ₄ ↑↑a * ↑χ₈ ↑a
exact χ₈'_eq_χ₄_mul_χ₈ a
no goals
a : ℤ
⊢ 4 ∣ 8
norm_num