まだ小学生の頃に習ったことで印象に残っているのは３の倍数の確認方法でした。各桁を足した数が３の倍数ならば元の数も３の倍数、というアレです。 倍数とか約数とかがLean4で扱えるようになり、この３の倍数の確認方法の証明を書き下してみようと思いまし…